# HG changeset patch
# User wenzelm
# Date 883317536 -3600
# Node ID 749600cb5573a50ac6ff00fda8e751f411076f19
# Parent  3e56603fde068243d7c34cd16386cccec2805227
renamed Symtab.null to Symtab.empty;
renamed Symtan.extend_new to Symtab.extend;
renamed Symtan.DUPLICATE to Symtab.DUP;

diff -r 3e56603fde06 -r 749600cb5573 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Dec 28 14:58:06 1997 +0100
+++ b/src/Pure/sign.ML	Sun Dec 28 14:58:56 1997 +0100
@@ -263,7 +263,7 @@
 
 (* prepare data *)
 
-val empty_data = Data Symtab.null;
+val empty_data = Data Symtab.empty;
 
 fun merge_data (Data tab1, Data tab2) =
   let
@@ -290,7 +290,7 @@
 
 fun init_data_sg sg (Data tab) kind e ext mrg prt =
   Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))
-    handle Symtab.DUPLICATE _ => err_dup_init sg kind;
+    handle Symtab.DUP _ => err_dup_init sg kind;
 
 
 (* access data *)
@@ -373,13 +373,14 @@
 
 (*add names*)
 fun add_names spaces kind names =
-  let val space' = NameSpace.extend (names, space_of spaces kind) in
+  let val space' = NameSpace.extend (space_of spaces kind, names) in
     overwrite (spaces, (kind, space'))
   end;
 
 (*make full names*)
 fun full path name =
-  if NameSpace.qualified name then
+  if name = "" then error "Attempt to declare empty name \"\""
+  else if NameSpace.qualified name then
     error ("Attempt to declare qualified name " ^ quote name)
   else NameSpace.pack (path @ [name]);
 
@@ -739,7 +740,7 @@
       else decls_of path Syntax.const_name consts;
   in
     (Syntax.extend_const_gram syn prmode consts, tsig,
-      Symtab.extend_new (ctab, decls)
+      Symtab.extend (ctab, decls)
         handle Symtab.DUPS cs => err_dup_consts cs,
       (path, add_names spaces constK (map fst decls)), data)
   end;
@@ -935,11 +936,11 @@
 (** partial Pure signature **)
 
 val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
-  Symtab.null, Syntax.pure_syn, [], [], empty_data, []);
+  Symtab.empty, Syntax.pure_syn, [], [], empty_data, []);
 
 val pre_pure =
   create_sign (SgRef (Some (ref dummy_sg))) [] "#"
-    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), empty_data);
+    (Syntax.pure_syn, Type.tsig0, Symtab.empty, ([], []), empty_data);
 
 
 end;