# HG changeset patch
# User wenzelm
# Date 883317404 -3600
# Node ID 9b4c1db5aca170201dfd1f43b7863d9b9af7e0ea
# Parent  48e4fbc03b7c1f329150fd9fc21861f0f58819b3
renamed Symtab.null to Symtab.empty;

diff -r 48e4fbc03b7c -r 9b4c1db5aca1 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sun Dec 28 14:56:09 1997 +0100
+++ b/src/Pure/Syntax/parser.ML	Sun Dec 28 14:56:44 1997 +0100
@@ -427,7 +427,7 @@
 
 (*The mother of all grammars*)
 val empty_gram = Gram {nt_count = 0, prod_count = 0,
-                       tags = Symtab.null, chains = [], lambdas = [],
+                       tags = Symtab.empty, chains = [], lambdas = [],
                        prods = Array.array (0, (([], []), []))};
 
 
diff -r 48e4fbc03b7c -r 9b4c1db5aca1 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sun Dec 28 14:56:09 1997 +0100
+++ b/src/Pure/Syntax/printer.ML	Sun Dec 28 14:56:44 1997 +0100
@@ -189,7 +189,7 @@
 
 (*find tab for mode*)
 fun get_tab prtabs mode =
-  if_none (assoc (prtabs, mode)) Symtab.null;
+  if_none (assoc (prtabs, mode)) Symtab.empty;
 
 (*collect tabs for mode hierarchy (default "")*)
 fun tabs_of prtabs modes =
diff -r 48e4fbc03b7c -r 9b4c1db5aca1 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Dec 28 14:56:09 1997 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Dec 28 14:56:44 1997 +0100
@@ -81,10 +81,10 @@
 fun err_dup_trfuns name cs =
   error ("More than one " ^ name ^ " for " ^ commas_quote cs);
 
-val empty_trtab = Symtab.null;
+val empty_trtab = Symtab.empty;
 
 fun extend_trtab tab trfuns name =
-  Symtab.extend_new (tab, map (fn (c, f) => (c, (f, stamp ()))) trfuns)
+  Symtab.extend (tab, map (fn (c, f) => (c, (f, stamp ()))) trfuns)
     handle Symtab.DUPS cs => err_dup_trfuns name cs;
 
 fun merge_trtabs tab1 tab2 name =
@@ -140,13 +140,13 @@
 (* lookup_ruletab *)
 
 fun lookup_ruletab tab =
-  if Symtab.is_null tab then None
+  if Symtab.is_empty tab then None
   else Some (fn a => Symtab.lookup_multi (tab, a));
 
 
 (* empty, extend, merge ruletabs *)
 
-val empty_ruletab = Symtab.null;
+val empty_ruletab = Symtab.empty;
 
 fun extend_ruletab tab rules =
   generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab
diff -r 48e4fbc03b7c -r 9b4c1db5aca1 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Dec 28 14:56:09 1997 +0100
+++ b/src/Pure/pure_thy.ML	Sun Dec 28 14:56:44 1997 +0100
@@ -50,7 +50,7 @@
 
 fun mk_empty _ =
   Theorems (ref {space = NameSpace.empty,
-    thms_tab = Symtab.null, const_idx = (0, Symtab.null)});
+    thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)});
 
 fun print sg (Theorems (ref {space, thms_tab, const_idx = _})) =
   let
@@ -143,7 +143,7 @@
   in (next + 1, foldl add (table, consts)) end;
 
 fun make_const_idx thm_tab =
-  foldl (foldl add_const_idx) ((0, Symtab.null), map snd (Symtab.dest thm_tab));
+  foldl (foldl add_const_idx) ((0, Symtab.empty), map snd (Symtab.dest thm_tab));
 
 
 (* lookup index *)
@@ -203,7 +203,7 @@
             (warn_same name; false)
           else (warn_overwrite name; true));
 
-    val space' = NameSpace.extend ([name], space);
+    val space' = NameSpace.extend (space, [name]);
     val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
     val const_idx' =
       if overwrite then make_const_idx thms_tab'
diff -r 48e4fbc03b7c -r 9b4c1db5aca1 src/Pure/term.ML
--- 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