--- 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' *)
--- 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 *)
--- 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));
--- 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;
--- 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;
--- 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) =
--- 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;
--- 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)
--- 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);