# HG changeset patch
# User wenzelm
# Date 883317278 -3600
# Node ID caf8ae95c61f82e7ac7efee8f2d8013d75f9fc2d
# Parent  43620c417579936c8df43ebe64955ed0fdbe4283
renamed (is_)null to (is_)empty;
renamed DUPLICATE to DUP;
renamed extend_new to extend;

diff -r 43620c417579 -r caf8ae95c61f src/Pure/symtab.ML
--- a/src/Pure/symtab.ML	Sat Dec 27 21:49:45 1997 +0100
+++ b/src/Pure/symtab.ML	Sun Dec 28 14:54:38 1997 +0100
@@ -8,11 +8,11 @@
 
 signature SYMTAB =
 sig
-  exception DUPLICATE of string
+  exception DUP of string
   exception DUPS of string list
   type 'a table
-  val null: 'a table
-  val is_null: 'a table -> bool
+  val empty: 'a table
+  val is_empty: 'a table -> bool
   val lookup: 'a table * string -> 'a option
   val find_first: (string * 'a -> bool) -> 'a table -> (string * 'a) option
   val update: (string * 'a) * 'a table -> 'a table
@@ -22,8 +22,7 @@
   val st_of_declist: (string list * 'a) list * 'a table -> 'a table
   val make: (string * 'a) list -> 'a table
   val dest: 'a table -> (string * 'a) list
-  val extend: ('a * 'a -> bool) -> 'a table * (string * 'a) list -> 'a table
-  val extend_new: 'a table * (string * 'a) list -> 'a table
+  val extend: 'a table * (string * 'a) list -> 'a table
   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
   val lookup_multi: 'a list table * string -> 'a list
   val make_multi: (string * 'a) list -> 'a list table
@@ -34,16 +33,16 @@
 struct
 
 (*symbol table errors, such as from update_new*)
-exception DUPLICATE of string;
+exception DUP of string;
 exception DUPS of string list;
 
 datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
 
 
-val null = Tip;
+val empty = Tip;
 
-fun is_null Tip = true
-  | is_null _ = false;
+fun is_empty Tip = true
+  | is_empty _ = false;
 
 
 fun lookup (symtab: 'a table, key: string) : 'a option =
@@ -81,7 +80,7 @@
         | upd (Branch(key', entry', left, right)) =
             if      key < key' then Branch (key', entry', upd left, right)
             else if key' < key then Branch (key', entry', left, upd right)
-            else  raise DUPLICATE(key)
+            else  raise DUP(key)
   in  upd symtab  end;
 
 
@@ -133,10 +132,10 @@
     [] => balance (foldr update_new (alst, Tip))
   | dups => raise DUPS (map fst dups));
 
-fun extend eq (tab, alst) =
+fun pre_extend eq (tab, alst) =
   generic_extend (eq_pair eq) dest make tab alst;
 
-fun extend_new (tab, alst) = extend (K false) (tab, alst);
+fun extend (tab, alst) = pre_extend (K false) (tab, alst);
 
 fun merge eq (tab1, tab2) =
   generic_merge (eq_pair eq) dest make tab1 tab2;