removed Table.extend, NameSpace.extend_table
authorhaftmann
Fri Dec 05 18:42:37 2008 +0100 (2008-12-05)
changeset 29004a5a91f387791
parent 28994 49f602ae24e5
child 29005 ce378dcfddab
removed Table.extend, NameSpace.extend_table
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/Pure/General/name_space.ML
src/Pure/General/table.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Syntax/syntax.ML
src/Pure/theory.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Fri Dec 05 18:42:37 2008 +0100
     1.3 @@ -346,19 +346,14 @@
     1.4  val get_updates = Symtab.lookup o #updates o get_sel_upd;
     1.5  fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
     1.6  
     1.7 -fun put_sel_upd names simps thy =
     1.8 -  let
     1.9 -    val sels = map (rpair ()) names;
    1.10 -    val upds = map (suffix updateN) names ~~ names;
    1.11 -
    1.12 -    val {records, sel_upd = {selectors, updates, simpset},
    1.13 -      equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
    1.14 -    val data = make_record_data records
    1.15 -      {selectors = Symtab.extend (selectors, sels),
    1.16 -        updates = Symtab.extend (updates, upds),
    1.17 -        simpset = Simplifier.addsimps (simpset, simps)}
    1.18 -       equalities extinjects extsplit splits extfields fieldext;
    1.19 -  in RecordsData.put data thy end;
    1.20 +fun put_sel_upd names simps = RecordsData.map (fn {records,
    1.21 +  sel_upd = {selectors, updates, simpset},
    1.22 +    equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    1.23 +  make_record_data records
    1.24 +    {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
    1.25 +      updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
    1.26 +      simpset = Simplifier.addsimps (simpset, simps)}
    1.27 +      equalities extinjects extsplit splits extfields fieldext);
    1.28  
    1.29  
    1.30  (* access 'equalities' *)
     2.1 --- a/src/HOL/Tools/refute.ML	Fri Dec 05 11:42:27 2008 +0100
     2.2 +++ b/src/HOL/Tools/refute.ML	Fri Dec 05 18:42:37 2008 +0100
     2.3 @@ -313,18 +313,10 @@
     2.4  
     2.5    (* (string * string) -> theory -> theory *)
     2.6  
     2.7 -  fun set_default_param (name, value) thy =
     2.8 -  let
     2.9 -    val {interpreters, printers, parameters} = RefuteData.get thy
    2.10 -  in
    2.11 -    RefuteData.put (case Symtab.lookup parameters name of
    2.12 -      NONE   =>
    2.13 +  fun set_default_param (name, value) = RefuteData.map 
    2.14 +    (fn {interpreters, printers, parameters} =>
    2.15        {interpreters = interpreters, printers = printers,
    2.16 -        parameters = Symtab.extend (parameters, [(name, value)])}
    2.17 -    | SOME _ =>
    2.18 -      {interpreters = interpreters, printers = printers,
    2.19 -        parameters = Symtab.update (name, value) parameters}) thy
    2.20 -  end;
    2.21 +        parameters = Symtab.update (name, value) parameters});
    2.22  
    2.23  (* ------------------------------------------------------------------------- *)
    2.24  (* get_default_param: retrieves the value associated with 'name' from        *)
     3.1 --- a/src/Pure/General/name_space.ML	Fri Dec 05 11:42:27 2008 +0100
     3.2 +++ b/src/Pure/General/name_space.ML	Fri Dec 05 18:42:37 2008 +0100
     3.3 @@ -48,7 +48,6 @@
     3.4      -> 'a table * 'a table -> 'a table
     3.5    val dest_table: 'a table -> (string * 'a) list
     3.6    val extern_table: 'a table -> (xstring * 'a) list
     3.7 -  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
     3.8  end;
     3.9  
    3.10  structure NameSpace: NAME_SPACE =
    3.11 @@ -303,10 +302,6 @@
    3.12      val (name, space') = declare naming b space;
    3.13    in (name, (space', Symtab.update_new (name, x) tab)) end;
    3.14  
    3.15 -fun extend_table naming bentries (space, tab) =
    3.16 -  let val entries = map (apfst (full_internal naming)) bentries
    3.17 -  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
    3.18 -
    3.19  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
    3.20    (merge (space1, space2), Symtab.merge eq (tab1, tab2));
    3.21  
     4.1 --- a/src/Pure/General/table.ML	Fri Dec 05 11:42:27 2008 +0100
     4.2 +++ b/src/Pure/General/table.ML	Fri Dec 05 18:42:37 2008 +0100
     4.3 @@ -41,7 +41,6 @@
     4.4    val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
     4.5    val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
     4.6    val make: (key * 'a) list -> 'a table                                (*exception DUP*)
     4.7 -  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUP*)
     4.8    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     4.9      'a table * 'a table -> 'a table                                    (*exception DUP*)
    4.10    val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
    4.11 @@ -364,9 +363,7 @@
    4.12  
    4.13  (* simultaneous modifications *)
    4.14  
    4.15 -fun extend (table, args) = fold update_new args table;
    4.16 -
    4.17 -fun make entries = extend (empty, entries);
    4.18 +fun make entries = fold update_new entries empty;
    4.19  
    4.20  fun join f (table1, table2) =
    4.21    let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
     5.1 --- a/src/Pure/Isar/attrib.ML	Fri Dec 05 11:42:27 2008 +0100
     5.2 +++ b/src/Pure/Isar/attrib.ML	Fri Dec 05 18:42:37 2008 +0100
     5.3 @@ -146,8 +146,8 @@
     5.4  fun add_attributes raw_attrs thy =
     5.5    let
     5.6      val new_attrs =
     5.7 -      raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
     5.8 -    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
     5.9 +      raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
    5.10 +    fun add attrs = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_attrs attrs
    5.11        handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
    5.12    in Attributes.map add thy end;
    5.13  
     6.1 --- a/src/Pure/Isar/locale.ML	Fri Dec 05 11:42:27 2008 +0100
     6.2 +++ b/src/Pure/Isar/locale.ML	Fri Dec 05 18:42:37 2008 +0100
     6.3 @@ -646,7 +646,7 @@
     6.4        | unify _ env = env;
     6.5      val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
     6.6      val Vs = map (Option.map (Envir.norm_type unifier)) Us';
     6.7 -    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
     6.8 +    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
     6.9    in map (Option.map (Envir.norm_type unifier')) Vs end;
    6.10  
    6.11  fun params_of elemss =
    6.12 @@ -711,7 +711,7 @@
    6.13        (Vartab.empty, maxidx);
    6.14  
    6.15      val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
    6.16 -    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
    6.17 +    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
    6.18  
    6.19      fun inst_parms (i, ps) =
    6.20        List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
    6.21 @@ -1100,15 +1100,15 @@
    6.22  *)
    6.23  
    6.24  fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
    6.25 -        val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
    6.26 +        val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
    6.27        in
    6.28          ((ids',
    6.29           merge_syntax ctxt ids'
    6.30 -           (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
    6.31 +           (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
    6.32             handle Symtab.DUP x => err_in_locale ctxt
    6.33               ("Conflicting syntax for parameter: " ^ quote x)
    6.34               (map #1 ids')),
    6.35 -         [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
    6.36 +         [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
    6.37        end
    6.38    | flatten _ ((ids, syn), Elem elem) =
    6.39        ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
    6.40 @@ -1252,7 +1252,7 @@
    6.41  
    6.42  
    6.43  fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
    6.44 -      let val x = Name.name_of b
    6.45 +      let val x = Binding.base_name b
    6.46        in (b, AList.lookup (op =) parms x, mx) end) fixes)
    6.47    | finish_ext_elem parms _ (Constrains _, _) = Constrains []
    6.48    | finish_ext_elem _ close (Assumes asms, propp) =
     7.1 --- a/src/Pure/Isar/method.ML	Fri Dec 05 11:42:27 2008 +0100
     7.2 +++ b/src/Pure/Isar/method.ML	Fri Dec 05 18:42:37 2008 +0100
     7.3 @@ -448,9 +448,9 @@
     7.4  fun add_methods raw_meths thy =
     7.5    let
     7.6      val new_meths = raw_meths |> map (fn (name, f, comment) =>
     7.7 -      (name, ((f, comment), stamp ())));
     7.8 +      (Binding.name name, ((f, comment), stamp ())));
     7.9  
    7.10 -    fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
    7.11 +    fun add meths = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_meths meths
    7.12        handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
    7.13    in Methods.map add thy end;
    7.14  
     8.1 --- a/src/Pure/Syntax/syntax.ML	Fri Dec 05 11:42:27 2008 +0100
     8.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Dec 05 18:42:37 2008 +0100
     8.3 @@ -173,7 +173,7 @@
     8.4  
     8.5  fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
     8.6  
     8.7 -fun update_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
     8.8 +fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
     8.9    handle Symtab.DUP c => err_dup_trfun name c;
    8.10  
    8.11  fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
     9.1 --- a/src/Pure/theory.ML	Fri Dec 05 11:42:27 2008 +0100
     9.2 +++ b/src/Pure/theory.ML	Fri Dec 05 18:42:37 2008 +0100
     9.3 @@ -178,8 +178,8 @@
     9.4  
     9.5  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
     9.6    let
     9.7 -    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
     9.8 -    val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
     9.9 +    val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
    9.10 +    val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
    9.11        handle Symtab.DUP dup => err_dup_axm dup;
    9.12    in axioms' end);
    9.13