--- a/src/Pure/term.ML Sun Dec 28 14:56:09 1997 +0100
+++ b/src/Pure/term.ML Sun Dec 28 14:56:44 1997 +0100
@@ -943,7 +943,7 @@
fun type_tag (Type("fun",[S,T])) = atomic_tag S ^ type_tag T
| type_tag T = atomic_tag T;
-val memo_types = ref (Symtab.null : typ list Symtab.table);
+val memo_types = ref (Symtab.empty : typ list Symtab.table);
(* special case of library/find_first *)
fun find_type (T, []: typ list) = None
@@ -973,7 +973,7 @@
(** Sharing of atomic terms **)
-val memo_terms = ref (Symtab.null : term list Symtab.table);
+val memo_terms = ref (Symtab.empty : term list Symtab.table);
(* special case of library/find_first *)
fun find_term (t, []: term list) = None