renamed Symtab.null to Symtab.empty;
authorwenzelm
Sun Dec 28 14:56:44 1997 +0100 (1997-12-28)
changeset 44879b4c1db5aca1
parent 4486 48e4fbc03b7c
child 4488 3e56603fde06
renamed Symtab.null to Symtab.empty;
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/pure_thy.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/Syntax/parser.ML	Sun Dec 28 14:56:09 1997 +0100
     1.2 +++ b/src/Pure/Syntax/parser.ML	Sun Dec 28 14:56:44 1997 +0100
     1.3 @@ -427,7 +427,7 @@
     1.4  
     1.5  (*The mother of all grammars*)
     1.6  val empty_gram = Gram {nt_count = 0, prod_count = 0,
     1.7 -                       tags = Symtab.null, chains = [], lambdas = [],
     1.8 +                       tags = Symtab.empty, chains = [], lambdas = [],
     1.9                         prods = Array.array (0, (([], []), []))};
    1.10  
    1.11  
     2.1 --- a/src/Pure/Syntax/printer.ML	Sun Dec 28 14:56:09 1997 +0100
     2.2 +++ b/src/Pure/Syntax/printer.ML	Sun Dec 28 14:56:44 1997 +0100
     2.3 @@ -189,7 +189,7 @@
     2.4  
     2.5  (*find tab for mode*)
     2.6  fun get_tab prtabs mode =
     2.7 -  if_none (assoc (prtabs, mode)) Symtab.null;
     2.8 +  if_none (assoc (prtabs, mode)) Symtab.empty;
     2.9  
    2.10  (*collect tabs for mode hierarchy (default "")*)
    2.11  fun tabs_of prtabs modes =
     3.1 --- a/src/Pure/Syntax/syntax.ML	Sun Dec 28 14:56:09 1997 +0100
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Dec 28 14:56:44 1997 +0100
     3.3 @@ -81,10 +81,10 @@
     3.4  fun err_dup_trfuns name cs =
     3.5    error ("More than one " ^ name ^ " for " ^ commas_quote cs);
     3.6  
     3.7 -val empty_trtab = Symtab.null;
     3.8 +val empty_trtab = Symtab.empty;
     3.9  
    3.10  fun extend_trtab tab trfuns name =
    3.11 -  Symtab.extend_new (tab, map (fn (c, f) => (c, (f, stamp ()))) trfuns)
    3.12 +  Symtab.extend (tab, map (fn (c, f) => (c, (f, stamp ()))) trfuns)
    3.13      handle Symtab.DUPS cs => err_dup_trfuns name cs;
    3.14  
    3.15  fun merge_trtabs tab1 tab2 name =
    3.16 @@ -140,13 +140,13 @@
    3.17  (* lookup_ruletab *)
    3.18  
    3.19  fun lookup_ruletab tab =
    3.20 -  if Symtab.is_null tab then None
    3.21 +  if Symtab.is_empty tab then None
    3.22    else Some (fn a => Symtab.lookup_multi (tab, a));
    3.23  
    3.24  
    3.25  (* empty, extend, merge ruletabs *)
    3.26  
    3.27 -val empty_ruletab = Symtab.null;
    3.28 +val empty_ruletab = Symtab.empty;
    3.29  
    3.30  fun extend_ruletab tab rules =
    3.31    generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab
     4.1 --- a/src/Pure/pure_thy.ML	Sun Dec 28 14:56:09 1997 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Sun Dec 28 14:56:44 1997 +0100
     4.3 @@ -50,7 +50,7 @@
     4.4  
     4.5  fun mk_empty _ =
     4.6    Theorems (ref {space = NameSpace.empty,
     4.7 -    thms_tab = Symtab.null, const_idx = (0, Symtab.null)});
     4.8 +    thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)});
     4.9  
    4.10  fun print sg (Theorems (ref {space, thms_tab, const_idx = _})) =
    4.11    let
    4.12 @@ -143,7 +143,7 @@
    4.13    in (next + 1, foldl add (table, consts)) end;
    4.14  
    4.15  fun make_const_idx thm_tab =
    4.16 -  foldl (foldl add_const_idx) ((0, Symtab.null), map snd (Symtab.dest thm_tab));
    4.17 +  foldl (foldl add_const_idx) ((0, Symtab.empty), map snd (Symtab.dest thm_tab));
    4.18  
    4.19  
    4.20  (* lookup index *)
    4.21 @@ -203,7 +203,7 @@
    4.22              (warn_same name; false)
    4.23            else (warn_overwrite name; true));
    4.24  
    4.25 -    val space' = NameSpace.extend ([name], space);
    4.26 +    val space' = NameSpace.extend (space, [name]);
    4.27      val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
    4.28      val const_idx' =
    4.29        if overwrite then make_const_idx thms_tab'
     5.1 --- a/src/Pure/term.ML	Sun Dec 28 14:56:09 1997 +0100
     5.2 +++ b/src/Pure/term.ML	Sun Dec 28 14:56:44 1997 +0100
     5.3 @@ -943,7 +943,7 @@
     5.4  fun type_tag (Type("fun",[S,T])) = atomic_tag S ^ type_tag T
     5.5    | type_tag T = atomic_tag T;
     5.6  
     5.7 -val memo_types = ref (Symtab.null : typ list Symtab.table);
     5.8 +val memo_types = ref (Symtab.empty : typ list Symtab.table);
     5.9  
    5.10  (* special case of library/find_first *)
    5.11  fun find_type (T, []: typ list) = None
    5.12 @@ -973,7 +973,7 @@
    5.13  
    5.14  (** Sharing of atomic terms **)
    5.15  
    5.16 -val memo_terms = ref (Symtab.null : term list Symtab.table);
    5.17 +val memo_terms = ref (Symtab.empty : term list Symtab.table);
    5.18  
    5.19  (* special case of library/find_first *)
    5.20  fun find_term (t, []: term list) = None