src/Pure/term.ML

   | atomic_tag (TVar ((a,_),_)) = a;
 
 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
   | find_type (T, T'::Ts) =
        if T=T' then Some T'

       let val Type (a,Ts) = T
       in  Type (a, map compress_type Ts)  end;
 
 (** 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
   | find_term (t, t'::ts) =
        if t=t' then Some t'