tuned Pure/General/name_space.ML

--- a/src/Pure/General/name_space.ML	Thu May 24 07:27:44 2007 +0200
+++ b/src/Pure/General/name_space.ML	Thu May 24 08:37:37 2007 +0200
@@ -53,7 +53,7 @@
     naming -> naming
   type 'a table (*= T * 'a Symtab.table*)
   val empty_table: 'a table
-  val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
+  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
@@ -169,11 +169,8 @@
 (* basic operations *)
 
 fun map_space f xname (NameSpace tab) =
-  let val entry' =
-    (case Symtab.lookup tab xname of
-      NONE => f ([], [])
-    | SOME (entry, _) => f entry)
-  in NameSpace (Symtab.update (xname, (entry', stamp ())) tab) end;
+  NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
+    (fn (entry, _) => (f entry, stamp ())) tab);
 
 fun del (name: string) = remove (op =) name;
 fun add name names = name :: del name names;
@@ -270,7 +267,7 @@
 
 val empty_table = (empty, Symtab.empty);
 
-fun extend_table naming ((space, tab), bentries) =
+fun extend_table naming bentries (space, tab) =
   let val entries = map (apfst (full naming)) bentries
   in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
 

--- a/src/Pure/Isar/attrib.ML	Thu May 24 07:27:44 2007 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu May 24 08:37:37 2007 +0200
@@ -127,7 +127,7 @@
   let
     val new_attrs =
       raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
-    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) (attrs, new_attrs)
+    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
       handle Symtab.DUPS dups =>
         error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
   in AttributesData.map add thy end;

--- a/src/Pure/Isar/method.ML	Thu May 24 07:27:44 2007 +0200
+++ b/src/Pure/Isar/method.ML	Thu May 24 08:37:37 2007 +0200
@@ -423,7 +423,7 @@
     val new_meths = raw_meths |> map (fn (name, f, comment) =>
       (name, ((f, comment), stamp ())));
 
-    fun add meths = NameSpace.extend_table (Sign.naming_of thy) (meths, new_meths)
+    fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
       handle Symtab.DUPS dups =>
         error ("Duplicate declaration of method(s) " ^ commas_quote dups);
   in MethodsData.map add thy end;

--- a/src/Pure/consts.ML	Thu May 24 07:27:44 2007 +0200
+++ b/src/Pure/consts.ML	Thu May 24 08:37:37 2007 +0200
@@ -202,7 +202,7 @@
 fun err_inconsistent_constraints cs =
   error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
 
-fun extend_decls naming decl tab = NameSpace.extend_table naming (tab, [decl])
+fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab
   handle Symtab.DUPS cs => err_dup_consts cs;
 
 

--- a/src/Pure/simplifier.ML	Thu May 24 07:27:44 2007 +0200
+++ b/src/Pure/simplifier.ML	Thu May 24 08:37:37 2007 +0200
@@ -228,7 +228,7 @@
       in
         context
         |> Simprocs.map (fn simprocs =>
-            NameSpace.extend_table naming (simprocs, [(name', simproc')])
+            NameSpace.extend_table naming [(name', simproc')] simprocs
               handle Symtab.DUPS ds => err_dup_simprocs ds)
         |> map_ss (fn ss => ss addsimprocs [simproc'])
       end)

--- a/src/Pure/theory.ML	Thu May 24 07:27:44 2007 +0200
+++ b/src/Pure/theory.ML	Thu May 24 08:37:37 2007 +0200
@@ -181,7 +181,7 @@
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
     val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
-    val axioms' = NameSpace.extend_table (Sign.naming_of thy) (axioms, axms)
+    val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
       handle Symtab.DUPS dups => err_dup_axms dups;
   in axioms' end);
 
@@ -306,7 +306,7 @@
 (** add oracle **)
 
 fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
-  NameSpace.extend_table (Sign.naming_of thy) (oracles, [(bname, (oracle, stamp ()))])
+  NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
     handle Symtab.DUPS dups => err_dup_oras dups);
 
 end;