--- 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, (([], []), []))};
--- 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 =
--- 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
--- 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'
--- 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