diff --git a/src/Pure/term_items.ML b/src/Pure/term_items.ML
--- a/src/Pure/term_items.ML
+++ b/src/Pure/term_items.ML
@@ -1,198 +1,198 @@
 (*  Title:      Pure/term_items.ML
     Author:     Makarius
 
 Scalable collections of term items:
   - table: e.g. for instantiation
   - set with order of addition, e.g. occurrences within term
 *)
 
 signature TERM_ITEMS =
 sig
+  structure Key: KEY
   type key
   type 'a table
   val empty: 'a table
   val build: ('a table -> 'a table) -> 'a table
   val size: 'a table -> int
   val is_empty: 'a table -> bool
   val map: (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val forall: (key * 'a -> bool) -> 'a table -> bool
   val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val lookup: 'a table -> key -> 'a option
   val defined: 'a table -> key -> bool
   val add: key * 'a -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table
   type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
   val list_set: set -> key list
   val list_set_rev: set -> key list
   val subset: set * set -> bool
   val eq_set: set * set -> bool
 end;
 
 functor Term_Items(Key: KEY): TERM_ITEMS =
 struct
 
+(* keys *)
+
+structure Key = Key;
+type key = Key.key;
+
+
 (* table with length *)
 
 structure Table = Table(Key);
 
-type key = Table.key;
-datatype 'a table = Items of int * 'a Table.table;
-
-fun size (Items (n, _)) = n;
-fun table (Items (_, tab)) = tab;
-
-val empty = Items (0, Table.empty);
-fun build (f: 'a table -> 'a table) = f empty;
-fun is_empty items = size items = 0;
+datatype 'a table = Table of 'a Table.table;
 
-fun dest items = Table.dest (table items);
-fun keys items = Table.keys (table items);
-fun exists pred = Table.exists pred o table;
-fun forall pred = Table.forall pred o table;
-fun get_first get = Table.get_first get o table;
-fun lookup items = Table.lookup (table items);
-fun defined items = Table.defined (table items);
+val empty = Table Table.empty;
+fun build (f: 'a table -> 'a table) = f empty;
+fun is_empty (Table tab) = Table.is_empty tab;
 
-fun add (key, x) (items as Items (n, tab)) =
-  if Table.defined tab key then items
-  else Items (n + 1, Table.update_new (key, x) tab);
+fun size (Table tab) = Table.size tab;
+fun dest (Table tab) = Table.dest tab;
+fun keys (Table tab) = Table.keys tab;
+fun exists pred (Table tab) = Table.exists pred tab;
+fun forall pred (Table tab) = Table.forall pred tab;
+fun get_first get (Table tab) = Table.get_first get tab;
+fun lookup (Table tab) = Table.lookup tab;
+fun defined (Table tab) = Table.defined tab;
 
+fun add entry (Table tab) = Table (Table.default entry tab);
 fun make entries = build (fold add entries);
 
 
 (* set with order of addition *)
 
 type set = int table;
 
-fun add_set x (items as Items (n, tab)) =
-  if Table.defined tab x then items
-  else Items (n + 1, Table.update_new (x, n) tab);
+fun add_set x (Table tab) =
+  Table (if Table.defined tab x then tab else Table.update_new (x, Table.size tab + 1) tab);
 
 fun make_set xs = build (fold add_set xs);
 
 fun subset (A: set, B: set) = forall (defined B o #1) A;
 fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
 
-fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1
+fun list_set_ord ord (Table tab) = tab |> Table.dest |> sort (ord o apply2 #2) |> map #1;
 val list_set = list_set_ord int_ord;
 val list_set_rev = list_set_ord (rev_order o int_ord);
 
-fun map f (Items (n, tab)) = Items (n, Table.map f tab);
-fun fold f = Table.fold f o table;
-fun fold_rev f = Table.fold_rev f o table;
+fun map f (Table tab) = Table (Table.map f tab);
+fun fold f (Table tab) = Table.fold f tab;
+fun fold_rev f (Table tab) = Table.fold_rev f tab;
 
 end;
 
 
 structure TFrees:
 sig
   include TERM_ITEMS
   val add_tfreesT: typ -> set -> set
   val add_tfrees: term -> set -> set
   val add_tfreesT_unless: (string * sort -> bool) -> typ -> set -> set
   val add_tfrees_unless: (string * sort -> bool) -> term -> set -> set
 end =
 struct
 
 structure Items = Term_Items
 (
   type key = string * sort;
   val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.sort_ord);
 );
 open Items;
 
 val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
 val add_tfrees = fold_types add_tfreesT;
 
 fun add_tfreesT_unless pred = Term.fold_atyps (fn TFree v => not (pred v) ? add_set v | _ => I);
 fun add_tfrees_unless pred = fold_types (add_tfreesT_unless pred);
 
 end;
 
 
 structure TVars:
 sig
   include TERM_ITEMS
   val add_tvarsT: typ -> set -> set
   val add_tvars: term -> set -> set
 end =
 struct
 
 structure Term_Items = Term_Items(
   type key = indexname * sort;
   val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord);
 );
 open Term_Items;
 
 val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I);
 val add_tvars = fold_types add_tvarsT;
 
 end;
 
 
 structure Frees:
 sig
   include TERM_ITEMS
   val add_frees: term -> set -> set
 end =
 struct
 
 structure Term_Items = Term_Items
 (
   type key = string * typ;
   val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.typ_ord);
 );
 open Term_Items;
 
 val add_frees = fold_aterms (fn Free v => add_set v | _ => I);
 
 end;
 
 
 structure Vars:
 sig
   include TERM_ITEMS
   val add_vars: term -> set -> set
 end =
 struct
 
 structure Term_Items = Term_Items
 (
   type key = indexname * typ;
   val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
 );
 open Term_Items;
 
 val add_vars = fold_aterms (fn Var v => add_set v | _ => I);
 
 end;
 
 
 structure Names:
 sig
   include TERM_ITEMS
   val add_tfree_namesT: typ -> set -> set
   val add_tfree_names: term -> set -> set
   val add_free_names: term -> set -> set
 end =
 struct
 
 structure Term_Items = Term_Items
 (
   type key = string;
   val ord = fast_string_ord
 );
 open Term_Items;
 
 val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I);
 val add_tfree_names = fold_types add_tfree_namesT;
 val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
 
 end;