# HG changeset patch
# User haftmann
# Date 1228498957 -3600
# Node ID a5a91f3877913ec6e576ef4882ea4415d8a6f72c
# Parent  49f602ae24e5bd2a0218bab22245321804c17f71
removed Table.extend, NameSpace.extend_table

diff -r 49f602ae24e5 -r a5a91f387791 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -346,19 +346,14 @@
 val get_updates = Symtab.lookup o #updates o get_sel_upd;
 fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
 
-fun put_sel_upd names simps thy =
-  let
-    val sels = map (rpair ()) names;
-    val upds = map (suffix updateN) names ~~ names;
-
-    val {records, sel_upd = {selectors, updates, simpset},
-      equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
-    val data = make_record_data records
-      {selectors = Symtab.extend (selectors, sels),
-        updates = Symtab.extend (updates, upds),
-        simpset = Simplifier.addsimps (simpset, simps)}
-       equalities extinjects extsplit splits extfields fieldext;
-  in RecordsData.put data thy end;
+fun put_sel_upd names simps = RecordsData.map (fn {records,
+  sel_upd = {selectors, updates, simpset},
+    equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+  make_record_data records
+    {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
+      updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
+      simpset = Simplifier.addsimps (simpset, simps)}
+      equalities extinjects extsplit splits extfields fieldext);
 
 
 (* access 'equalities' *)
diff -r 49f602ae24e5 -r a5a91f387791 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -313,18 +313,10 @@
 
   (* (string * string) -> theory -> theory *)
 
-  fun set_default_param (name, value) thy =
-  let
-    val {interpreters, printers, parameters} = RefuteData.get thy
-  in
-    RefuteData.put (case Symtab.lookup parameters name of
-      NONE   =>
+  fun set_default_param (name, value) = RefuteData.map 
+    (fn {interpreters, printers, parameters} =>
       {interpreters = interpreters, printers = printers,
-        parameters = Symtab.extend (parameters, [(name, value)])}
-    | SOME _ =>
-      {interpreters = interpreters, printers = printers,
-        parameters = Symtab.update (name, value) parameters}) thy
-  end;
+        parameters = Symtab.update (name, value) parameters});
 
 (* ------------------------------------------------------------------------- *)
 (* get_default_param: retrieves the value associated with 'name' from        *)
diff -r 49f602ae24e5 -r a5a91f387791 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/General/name_space.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -48,7 +48,6 @@
     -> 'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
-  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
 end;
 
 structure NameSpace: NAME_SPACE =
@@ -303,10 +302,6 @@
     val (name, space') = declare naming b space;
   in (name, (space', Symtab.update_new (name, x) tab)) end;
 
-fun extend_table naming bentries (space, tab) =
-  let val entries = map (apfst (full_internal naming)) bentries
-  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
-
 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.merge eq (tab1, tab2));
 
diff -r 49f602ae24e5 -r a5a91f387791 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/General/table.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -41,7 +41,6 @@
   val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
   val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table                                (*exception DUP*)
-  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a table * 'a table -> 'a table                                    (*exception DUP*)
   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
@@ -364,9 +363,7 @@
 
 (* simultaneous modifications *)
 
-fun extend (table, args) = fold update_new args table;
-
-fun make entries = extend (empty, entries);
+fun make entries = fold update_new entries empty;
 
 fun join f (table1, table2) =
   let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
diff -r 49f602ae24e5 -r a5a91f387791 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -146,8 +146,8 @@
 fun add_attributes raw_attrs thy =
   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) new_attrs attrs
+      raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
+    fun add attrs = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_attrs attrs
       handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
   in Attributes.map add thy end;
 
diff -r 49f602ae24e5 -r a5a91f387791 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -646,7 +646,7 @@
       | unify _ env = env;
     val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
-    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
+    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
   in map (Option.map (Envir.norm_type unifier')) Vs end;
 
 fun params_of elemss =
@@ -711,7 +711,7 @@
       (Vartab.empty, maxidx);
 
     val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
-    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
+    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
 
     fun inst_parms (i, ps) =
       List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
@@ -1100,15 +1100,15 @@
 *)
 
 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
-        val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
+        val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
       in
         ((ids',
          merge_syntax ctxt ids'
-           (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
+           (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
            handle Symtab.DUP x => err_in_locale ctxt
              ("Conflicting syntax for parameter: " ^ quote x)
              (map #1 ids')),
-         [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
+         [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
       end
   | flatten _ ((ids, syn), Elem elem) =
       ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
@@ -1252,7 +1252,7 @@
 
 
 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
-      let val x = Name.name_of b
+      let val x = Binding.base_name b
       in (b, AList.lookup (op =) parms x, mx) end) fixes)
   | finish_ext_elem parms _ (Constrains _, _) = Constrains []
   | finish_ext_elem _ close (Assumes asms, propp) =
diff -r 49f602ae24e5 -r a5a91f387791 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/Isar/method.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -448,9 +448,9 @@
 fun add_methods raw_meths thy =
   let
     val new_meths = raw_meths |> map (fn (name, f, comment) =>
-      (name, ((f, comment), stamp ())));
+      (Binding.name name, ((f, comment), stamp ())));
 
-    fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
+    fun add meths = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_meths meths
       handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
   in Methods.map add thy end;
 
diff -r 49f602ae24e5 -r a5a91f387791 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -173,7 +173,7 @@
 
 fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
 
-fun update_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
+fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
   handle Symtab.DUP c => err_dup_trfun name c;
 
 fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
diff -r 49f602ae24e5 -r a5a91f387791 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/theory.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -178,8 +178,8 @@
 
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
-    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
-    val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
+    val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
+    val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
       handle Symtab.DUP dup => err_dup_axm dup;
   in axioms' end);