binding replaces bstring
authorhaftmann
Wed Jan 21 16:47:04 2009 +0100 (2009-01-21 ago)
changeset 29579cb520b766e00
parent 29578 8c4e961fcb08
child 29580 117b88da143c
binding replaces bstring
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/old_primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typedef_package.ML
src/HOL/ex/Quickcheck.thy
src/Pure/Isar/calculation.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/overloading.ML
src/Pure/ML/ml_context.ML
src/Pure/Proof/extraction.ML
src/Pure/Tools/named_thms.ML
src/Pure/assumption.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
src/Pure/pure_thy.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Jan 21 16:47:03 2009 +0100
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Jan 21 16:47:04 2009 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4                            (wfrec $ map_types poly_tvars R)
     1.5                        $ functional
     1.6       val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
     1.7 -     val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy
     1.8 +     val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
     1.9   in (thy', def) end;
    1.10  end;
    1.11  
    1.12 @@ -549,7 +549,7 @@
    1.13       val ([def0], theory) =
    1.14         thy
    1.15         |> PureThy.add_defs false
    1.16 -            [Thm.no_attributes (fid ^ "_def", defn)]
    1.17 +            [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
    1.18       val def = Thm.freezeT def0;
    1.19       val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
    1.20                             else ()
     2.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Jan 21 16:47:03 2009 +0100
     2.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Jan 21 16:47:04 2009 +0100
     2.3 @@ -238,7 +238,7 @@
     2.4            (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
     2.5            (reccomb_names ~~ recTs ~~ rec_result_Ts))
     2.6        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
     2.7 -          ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
     2.8 +          (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
     2.9             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    2.10               set $ Free ("x", T) $ Free ("y", T'))))))
    2.11                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
    2.12 @@ -262,7 +262,7 @@
    2.13    in
    2.14      thy2
    2.15      |> Sign.add_path (space_implode "_" new_type_names)
    2.16 -    |> PureThy.add_thmss [(("recs", rec_thms), [])]
    2.17 +    |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [])]
    2.18      ||> Sign.parent_path
    2.19      ||> Theory.checkpoint
    2.20      |-> (fn thms => pair (reccomb_names, Library.flat thms))
    2.21 @@ -316,7 +316,7 @@
    2.22              fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
    2.23            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
    2.24            val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn);
    2.25 -          val def = ((Sign.base_name name) ^ "_def",
    2.26 +          val def = (Binding.name (Sign.base_name name ^ "_def"),
    2.27              Logic.mk_equals (list_comb (Const (name, caseT), fns1),
    2.28                list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
    2.29                  fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
     3.1 --- a/src/HOL/Tools/datatype_aux.ML	Wed Jan 21 16:47:03 2009 +0100
     3.2 +++ b/src/HOL/Tools/datatype_aux.ML	Wed Jan 21 16:47:04 2009 +0100
     3.3 @@ -76,7 +76,7 @@
     3.4  fun store_thmss_atts label tnames attss thmss =
     3.5    fold_map (fn ((tname, atts), thms) =>
     3.6      Sign.add_path tname
     3.7 -    #> PureThy.add_thmss [((label, thms), atts)]
     3.8 +    #> PureThy.add_thmss [((Binding.name label, thms), atts)]
     3.9      #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
    3.10    ##> Theory.checkpoint;
    3.11  
    3.12 @@ -85,7 +85,7 @@
    3.13  fun store_thms_atts label tnames attss thmss =
    3.14    fold_map (fn ((tname, atts), thms) =>
    3.15      Sign.add_path tname
    3.16 -    #> PureThy.add_thms [((label, thms), atts)]
    3.17 +    #> PureThy.add_thms [((Binding.name label, thms), atts)]
    3.18      #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
    3.19    ##> Theory.checkpoint;
    3.20  
     4.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Jan 21 16:47:03 2009 +0100
     4.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Jan 21 16:47:04 2009 +0100
     4.3 @@ -196,13 +196,13 @@
     4.4  
     4.5  fun add_rules simps case_thms rec_thms inject distinct
     4.6                    weak_case_congs cong_att =
     4.7 -  PureThy.add_thmss [(("simps", simps), []),
     4.8 -    (("", flat case_thms @
     4.9 +  PureThy.add_thmss [((Binding.name "simps", simps), []),
    4.10 +    ((Binding.empty, flat case_thms @
    4.11            flat distinct @ rec_thms), [Simplifier.simp_add]),
    4.12 -    (("", rec_thms), [Code.add_default_eqn_attribute]),
    4.13 -    (("", flat inject), [iff_add]),
    4.14 -    (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    4.15 -    (("", weak_case_congs), [cong_att])]
    4.16 +    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
    4.17 +    ((Binding.empty, flat inject), [iff_add]),
    4.18 +    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    4.19 +    ((Binding.empty, weak_case_congs), [cong_att])]
    4.20    #> snd;
    4.21  
    4.22  
    4.23 @@ -213,15 +213,15 @@
    4.24      val inducts = ProjectRule.projections (ProofContext.init thy) induction;
    4.25  
    4.26      fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
    4.27 -      [(("", nth inducts index), [Induct.induct_type name]),
    4.28 -       (("", exhaustion), [Induct.cases_type name])];
    4.29 +      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
    4.30 +       ((Binding.empty, exhaustion), [Induct.cases_type name])];
    4.31      fun unnamed_rule i =
    4.32 -      (("", nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
    4.33 +      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
    4.34    in
    4.35      thy |> PureThy.add_thms
    4.36        (maps named_rules infos @
    4.37          map unnamed_rule (length infos upto length inducts - 1)) |> snd
    4.38 -    |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd
    4.39 +    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
    4.40    end;
    4.41  
    4.42  
    4.43 @@ -451,7 +451,7 @@
    4.44        |> store_thmss "inject" new_type_names inject
    4.45        ||>> store_thmss "distinct" new_type_names distinct
    4.46        ||> Sign.add_path (space_implode "_" new_type_names)
    4.47 -      ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])];
    4.48 +      ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
    4.49  
    4.50      val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
    4.51        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
     5.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Jan 21 16:47:03 2009 +0100
     5.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Jan 21 16:47:04 2009 +0100
     5.3 @@ -130,7 +130,7 @@
     5.4      val vs = map (fn i => List.nth (pnames, i)) is;
     5.5      val (thm', thy') = thy
     5.6        |> Sign.absolute_path
     5.7 -      |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm)
     5.8 +      |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
     5.9        ||> Sign.restore_naming thy;
    5.10  
    5.11      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
    5.12 @@ -196,7 +196,7 @@
    5.13      val exh_name = Thm.get_name exhaustion;
    5.14      val (thm', thy') = thy
    5.15        |> Sign.absolute_path
    5.16 -      |> PureThy.store_thm (exh_name ^ "_P_correctness", thm)
    5.17 +      |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm)
    5.18        ||> Sign.restore_naming thy;
    5.19  
    5.20      val P = Var (("P", 0), rT' --> HOLogic.boolT);
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jan 21 16:47:03 2009 +0100
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jan 21 16:47:04 2009 +0100
     6.3 @@ -242,7 +242,7 @@
     6.4          val ([def_thm], thy') =
     6.5            thy
     6.6            |> Sign.add_consts_i [(cname', constrT, mx)]
     6.7 -          |> (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)];
     6.8 +          |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
     6.9  
    6.10        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    6.11  
    6.12 @@ -343,7 +343,7 @@
    6.13          
    6.14          val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
    6.15          val fTs = map fastype_of fs;
    6.16 -        val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
    6.17 +        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Sign.base_name iso_name ^ "_def"),
    6.18            Logic.mk_equals (Const (iso_name, T --> Univ_elT),
    6.19              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
    6.20          val (def_thms, thy') =
    6.21 @@ -631,7 +631,7 @@
    6.22      val ([dt_induct'], thy7) =
    6.23        thy6
    6.24        |> Sign.add_path big_name
    6.25 -      |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
    6.26 +      |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
    6.27        ||> Sign.parent_path
    6.28        ||> Theory.checkpoint;
    6.29  
     7.1 --- a/src/HOL/Tools/function_package/size.ML	Wed Jan 21 16:47:03 2009 +0100
     7.2 +++ b/src/HOL/Tools/function_package/size.ML	Wed Jan 21 16:47:04 2009 +0100
     7.3 @@ -144,7 +144,7 @@
     7.4             (size_names ~~ recTs1))
     7.5        |> PureThy.add_defs false
     7.6          (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
     7.7 -           (def_names ~~ (size_fns ~~ rec_combs1)))
     7.8 +           (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
     7.9        ||> TheoryTarget.instantiation
    7.10             (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
    7.11        ||>> fold_map define_overloaded
    7.12 @@ -208,7 +208,7 @@
    7.13        prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
    7.14  
    7.15      val ([size_thms], thy'') =  PureThy.add_thmss
    7.16 -      [(("size", size_eqns),
    7.17 +      [((Binding.name "size", size_eqns),
    7.18          [Simplifier.simp_add, Thm.declaration_attribute
    7.19                (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
    7.20  
     8.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Jan 21 16:47:03 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jan 21 16:47:04 2009 +0100
     8.3 @@ -391,14 +391,14 @@
     8.4             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
     8.5               [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
     8.6                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
     8.7 -        val (thm', thy') = PureThy.store_thm (space_implode "_"
     8.8 -          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
     8.9 +        val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
    8.10 +          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
    8.11          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
    8.12            (DatatypeAux.split_conj_thm thm');
    8.13          val ([thms'], thy'') = PureThy.add_thmss
    8.14 -          [((space_implode "_"
    8.15 +          [((Binding.name (space_implode "_"
    8.16               (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
    8.17 -               ["correctness"]), thms), [])] thy';
    8.18 +               ["correctness"])), thms), [])] thy';
    8.19          val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
    8.20        in
    8.21          Extraction.add_realizers_i
    8.22 @@ -451,8 +451,8 @@
    8.23             rewrite_goals_tac rews,
    8.24             REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
    8.25               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
    8.26 -        val (thm', thy') = PureThy.store_thm (space_implode "_"
    8.27 -          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
    8.28 +        val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
    8.29 +          (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
    8.30        in
    8.31          Extraction.add_realizers_i
    8.32            [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
     9.1 --- a/src/HOL/Tools/old_primrec_package.ML	Wed Jan 21 16:47:03 2009 +0100
     9.2 +++ b/src/HOL/Tools/old_primrec_package.ML	Wed Jan 21 16:47:04 2009 +0100
     9.3 @@ -305,11 +305,11 @@
     9.4    end;
     9.5  
     9.6  fun thy_note ((name, atts), thms) =
     9.7 -  PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
     9.8 +  PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
     9.9  fun thy_def false ((name, atts), t) =
    9.10 -      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
    9.11 +      PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
    9.12    | thy_def true ((name, atts), t) =
    9.13 -      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
    9.14 +      PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
    9.15  
    9.16  in
    9.17  
    10.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Jan 21 16:47:03 2009 +0100
    10.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Jan 21 16:47:04 2009 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/Tools/recdef_package.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Markus Wenzel, TU Muenchen
    10.7  
    10.8  Wrapper module for Konrad Slind's TFL package.
    10.9 @@ -16,10 +15,10 @@
   10.10    val cong_del: attribute
   10.11    val wf_add: attribute
   10.12    val wf_del: attribute
   10.13 -  val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
   10.14 +  val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
   10.15      Attrib.src option -> theory -> theory
   10.16        * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   10.17 -  val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
   10.18 +  val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
   10.19      theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   10.20    val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
   10.21      -> theory -> theory * {induct_rules: thm}
   10.22 @@ -214,8 +213,8 @@
   10.23        thy
   10.24        |> Sign.add_path bname
   10.25        |> PureThy.add_thmss
   10.26 -        ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   10.27 -      ||>> PureThy.add_thms [(("induct", induct), [])];
   10.28 +        (((Binding.name "simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   10.29 +      ||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
   10.30      val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
   10.31      val thy =
   10.32        thy
   10.33 @@ -243,7 +242,7 @@
   10.34      val ([induct_rules'], thy3) =
   10.35        thy2
   10.36        |> Sign.add_path bname
   10.37 -      |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
   10.38 +      |> PureThy.add_thms [((Binding.name "induct_rules", induct_rules), [])]
   10.39        ||> Sign.parent_path;
   10.40    in (thy3, {induct_rules = induct_rules'}) end;
   10.41  
   10.42 @@ -299,7 +298,7 @@
   10.43  
   10.44  val recdef_decl =
   10.45    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
   10.46 -  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
   10.47 +  P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
   10.48      -- Scan.option hints
   10.49    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
   10.50  
    11.1 --- a/src/HOL/Tools/record_package.ML	Wed Jan 21 16:47:03 2009 +0100
    11.2 +++ b/src/HOL/Tools/record_package.ML	Wed Jan 21 16:47:04 2009 +0100
    11.3 @@ -1534,8 +1534,10 @@
    11.4        |> extension_typedef name repT (alphas@[zeta])
    11.5        ||> Sign.add_consts_i
    11.6              (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
    11.7 -      ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
    11.8 -      ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
    11.9 +      ||>> PureThy.add_defs false
   11.10 +            (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
   11.11 +      ||>> PureThy.add_defs false
   11.12 +            (map (Thm.no_attributes o apfst Binding.name) upd_specs)
   11.13        |-> (fn args as ((_, dest_defs), upd_defs) =>
   11.14            fold Code.add_default_eqn dest_defs
   11.15            #> fold Code.add_default_eqn upd_defs
   11.16 @@ -1693,14 +1695,14 @@
   11.17            [dest_convs',upd_convs']),
   11.18        thm_thy) =
   11.19        defs_thy
   11.20 -      |> (PureThy.add_thms o map Thm.no_attributes)
   11.21 +      |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
   11.22             [("ext_inject", inject),
   11.23              ("ext_induct", induct),
   11.24              ("ext_cases", cases),
   11.25              ("ext_surjective", surjective),
   11.26              ("ext_split", split_meta)]
   11.27 -      ||>> (PureThy.add_thmss o map Thm.no_attributes)
   11.28 -              [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)]
   11.29 +      ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
   11.30 +            [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)]
   11.31  
   11.32    in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
   11.33    end;
   11.34 @@ -1938,9 +1940,9 @@
   11.35            (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
   11.36        |> (Sign.add_consts_i o map Syntax.no_syn)
   11.37            (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   11.38 -      |> ((PureThy.add_defs false o map Thm.no_attributes) sel_specs)
   11.39 -      ||>> ((PureThy.add_defs false o map Thm.no_attributes) upd_specs)
   11.40 -      ||>> ((PureThy.add_defs false o map Thm.no_attributes)
   11.41 +      |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
   11.42 +      ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
   11.43 +      ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
   11.44               [make_spec, fields_spec, extend_spec, truncate_spec])
   11.45        |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
   11.46            fold Code.add_default_eqn sel_defs
   11.47 @@ -2164,17 +2166,17 @@
   11.48      val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'],
   11.49              [surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) =
   11.50        defs_thy
   11.51 -      |> (PureThy.add_thmss o map Thm.no_attributes)
   11.52 +      |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
   11.53           [("select_convs", sel_convs_standard),
   11.54            ("update_convs", upd_convs),
   11.55            ("select_defs", sel_defs),
   11.56            ("update_defs", upd_defs),
   11.57            ("splits", [split_meta_standard,split_object,split_ex]),
   11.58            ("defs", derived_defs)]
   11.59 -      ||>> (PureThy.add_thms o map Thm.no_attributes)
   11.60 +      ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
   11.61            [("surjective", surjective),
   11.62             ("equality", equality)]
   11.63 -      ||>> PureThy.add_thms
   11.64 +      ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name)
   11.65          [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
   11.66           (("induct", induct), induct_type_global name),
   11.67           (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
   11.68 @@ -2186,8 +2188,8 @@
   11.69      val final_thy =
   11.70        thms_thy
   11.71        |> (snd oo PureThy.add_thmss)
   11.72 -          [(("simps", sel_upd_simps), [Simplifier.simp_add]),
   11.73 -           (("iffs",iffs), [iff_add])]
   11.74 +          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
   11.75 +           ((Binding.name "iffs", iffs), [iff_add])]
   11.76        |> put_record name (make_record_info args parent fields extension induct_scheme')
   11.77        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
   11.78        |> add_record_equalities extension_id equality'
    12.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Jan 21 16:47:03 2009 +0100
    12.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Jan 21 16:47:04 2009 +0100
    12.3 @@ -84,7 +84,7 @@
    12.4              val (c, thy') =
    12.5                Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy
    12.6              val cdef = cname ^ "_def"
    12.7 -            val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
    12.8 +            val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
    12.9              val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
   12.10            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
   12.11        | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
    13.1 --- a/src/HOL/Tools/specification_package.ML	Wed Jan 21 16:47:03 2009 +0100
    13.2 +++ b/src/HOL/Tools/specification_package.ML	Wed Jan 21 16:47:04 2009 +0100
    13.3 @@ -28,7 +28,7 @@
    13.4                                 else thname
    13.5                  val def_eq = Logic.mk_equals (Const(cname_full,ctype),
    13.6                                                HOLogic.choice_const ctype $  P)
    13.7 -                val (thms, thy') = PureThy.add_defs covld [((cdefname,def_eq),[])] thy
    13.8 +                val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
    13.9                  val thm' = [thm,hd thms] MRS @{thm exE_some}
   13.10              in
   13.11                  mk_definitional cos (thy',thm')
   13.12 @@ -39,7 +39,7 @@
   13.13          let
   13.14              fun process [] (thy,tm) =
   13.15                  let
   13.16 -                    val (thms, thy') = PureThy.add_axioms [((axname,HOLogic.mk_Trueprop tm),[])] thy
   13.17 +                    val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy
   13.18                  in
   13.19                      (thy',hd thms)
   13.20                  end
   13.21 @@ -184,7 +184,7 @@
   13.22                              if name = ""
   13.23                              then arg |> Library.swap
   13.24                              else (writeln ("  " ^ name ^ ": " ^ (Display.string_of_thm thm));
   13.25 -                                  PureThy.store_thm (name, thm) thy)
   13.26 +                                  PureThy.store_thm (Binding.name name, thm) thy)
   13.27                      in
   13.28                          args |> apsnd (remove_alls frees)
   13.29                               |> apsnd undo_imps
    14.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Jan 21 16:47:03 2009 +0100
    14.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Jan 21 16:47:04 2009 +0100
    14.3 @@ -112,7 +112,8 @@
    14.4        if def then
    14.5          theory
    14.6          |> Sign.add_consts_i [(name, setT', NoSyn)]
    14.7 -        |> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))]
    14.8 +        |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
    14.9 +            (PrimitiveDefs.mk_defpair (setC, set)))]
   14.10          |-> (fn [th] => pair (SOME th))
   14.11        else (NONE, theory);
   14.12      fun contract_def NONE th = th
   14.13 @@ -130,7 +131,7 @@
   14.14           (Abs_name, oldT --> newT, NoSyn)]
   14.15        #> add_def
   14.16        #-> (fn set_def =>
   14.17 -        PureThy.add_axioms [((typedef_name, typedef_prop),
   14.18 +        PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
   14.19            [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
   14.20          ##>> pair set_def)
   14.21        ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
   14.22 @@ -143,7 +144,7 @@
   14.23              thy1
   14.24              |> Sign.add_path name
   14.25              |> PureThy.add_thms
   14.26 -              ([((Rep_name, make @{thm type_definition.Rep}), []),
   14.27 +              ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []),
   14.28                  ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
   14.29                  ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
   14.30                  ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
    15.1 --- a/src/HOL/ex/Quickcheck.thy	Wed Jan 21 16:47:03 2009 +0100
    15.2 +++ b/src/HOL/ex/Quickcheck.thy	Wed Jan 21 16:47:04 2009 +0100
    15.3 @@ -200,7 +200,7 @@
    15.4              in
    15.5                lthy
    15.6                |> LocalTheory.theory (Code.del_eqns c
    15.7 -                   #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
    15.8 +                   #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal])
    15.9                     #-> Code.add_eqn)
   15.10              end;
   15.11          in
    16.1 --- a/src/Pure/Isar/calculation.ML	Wed Jan 21 16:47:03 2009 +0100
    16.2 +++ b/src/Pure/Isar/calculation.ML	Wed Jan 21 16:47:04 2009 +0100
    16.3 @@ -98,8 +98,8 @@
    16.4      ("sym", sym_att, "declaration of symmetry rule"),
    16.5      ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
    16.6    PureThy.add_thms
    16.7 -   [(("", transitive_thm), [trans_add]),
    16.8 -    (("", symmetric_thm), [sym_add])] #> snd));
    16.9 +   [((Binding.empty, transitive_thm), [trans_add]),
   16.10 +    ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
   16.11  
   16.12  
   16.13  
    17.1 --- a/src/Pure/Isar/constdefs.ML	Wed Jan 21 16:47:03 2009 +0100
    17.2 +++ b/src/Pure/Isar/constdefs.ML	Wed Jan 21 16:47:04 2009 +0100
    17.3 @@ -8,12 +8,12 @@
    17.4  
    17.5  signature CONSTDEFS =
    17.6  sig
    17.7 -  val add_constdefs: (Binding.T * string option) list *
    17.8 -    ((Binding.T * string option * mixfix) option *
    17.9 +  val add_constdefs: (binding * string option) list *
   17.10 +    ((binding * string option * mixfix) option *
   17.11        (Attrib.binding * string)) list -> theory -> theory
   17.12 -  val add_constdefs_i: (Binding.T * typ option) list *
   17.13 -    ((Binding.T * typ option * mixfix) option *
   17.14 -      ((Binding.T * attribute list) * term)) list -> theory -> theory
   17.15 +  val add_constdefs_i: (binding * typ option) list *
   17.16 +    ((binding * typ option * mixfix) option *
   17.17 +      ((binding * attribute list) * term)) list -> theory -> theory
   17.18  end;
   17.19  
   17.20  structure Constdefs: CONSTDEFS =
   17.21 @@ -52,7 +52,7 @@
   17.22      val thy' =
   17.23        thy
   17.24        |> Sign.add_consts_i [(c, T, mx)]
   17.25 -      |> PureThy.add_defs false [((name, def), atts)]
   17.26 +      |> PureThy.add_defs false [((Binding.name name, def), atts)]
   17.27        |-> (fn [thm] => Code.add_default_eqn thm);
   17.28    in ((c, T), thy') end;
   17.29  
    18.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 21 16:47:03 2009 +0100
    18.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 21 16:47:04 2009 +0100
    18.3 @@ -13,8 +13,8 @@
    18.4    val typed_print_translation: bool * (string * Position.T) -> theory -> theory
    18.5    val print_ast_translation: bool * (string * Position.T) -> theory -> theory
    18.6    val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
    18.7 -  val add_axioms: ((Binding.T * string) * Attrib.src list) list -> theory -> theory
    18.8 -  val add_defs: (bool * bool) * ((Binding.T * string) * Attrib.src list) list -> theory -> theory
    18.9 +  val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
   18.10 +  val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
   18.11    val declaration: string * Position.T -> local_theory -> local_theory
   18.12    val simproc_setup: string -> string list -> string * Position.T -> string list ->
   18.13      local_theory -> local_theory
   18.14 @@ -53,7 +53,6 @@
   18.15    val print_theorems: Toplevel.transition -> Toplevel.transition
   18.16    val print_locales: Toplevel.transition -> Toplevel.transition
   18.17    val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
   18.18 -  val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
   18.19    val print_attributes: Toplevel.transition -> Toplevel.transition
   18.20    val print_simpset: Toplevel.transition -> Toplevel.transition
   18.21    val print_rules: Toplevel.transition -> Toplevel.transition
   18.22 @@ -359,12 +358,6 @@
   18.23    Toplevel.keep (fn state =>
   18.24      Locale.print_locale (Toplevel.theory_of state) show_facts name);
   18.25  
   18.26 -fun print_registrations show_wits name = Toplevel.unknown_context o
   18.27 -  Toplevel.keep (Toplevel.node_case
   18.28 -      (Context.cases (Old_Locale.print_registrations show_wits name o ProofContext.init)
   18.29 -        (Old_Locale.print_registrations show_wits name))
   18.30 -    (Old_Locale.print_registrations show_wits name o Proof.context_of));
   18.31 -
   18.32  val print_attributes = Toplevel.unknown_theory o
   18.33    Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
   18.34  
    19.1 --- a/src/Pure/Isar/overloading.ML	Wed Jan 21 16:47:03 2009 +0100
    19.2 +++ b/src/Pure/Isar/overloading.ML	Wed Jan 21 16:47:04 2009 +0100
    19.3 @@ -134,8 +134,8 @@
    19.4  
    19.5  fun declare c_ty = pair (Const c_ty);
    19.6  
    19.7 -fun define checked name (c, t) =
    19.8 -  Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t));
    19.9 +fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name,
   19.10 +  Logic.mk_equals (Const (c, Term.fastype_of t), t));
   19.11  
   19.12  
   19.13  (* target *)
    20.1 --- a/src/Pure/ML/ml_context.ML	Wed Jan 21 16:47:03 2009 +0100
    20.2 +++ b/src/Pure/ML/ml_context.ML	Wed Jan 21 16:47:04 2009 +0100
    20.3 @@ -126,7 +126,8 @@
    20.4  
    20.5  fun ml_store sel (name, ths) =
    20.6    let
    20.7 -    val ths' = Context.>>> (Context.map_theory_result (PureThy.store_thms (name, ths)));
    20.8 +    val ths' = Context.>>> (Context.map_theory_result
    20.9 +      (PureThy.store_thms (Binding.name name, ths)));
   20.10      val _ =
   20.11        if name = "" then ()
   20.12        else if not (ML_Syntax.is_identifier name) then
    21.1 --- a/src/Pure/Proof/extraction.ML	Wed Jan 21 16:47:03 2009 +0100
    21.2 +++ b/src/Pure/Proof/extraction.ML	Wed Jan 21 16:47:04 2009 +0100
    21.3 @@ -733,11 +733,11 @@
    21.4               val (def_thms, thy') = if t = nullt then ([], thy) else
    21.5                 thy
    21.6                 |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
    21.7 -               |> PureThy.add_defs false [((extr_name s vs ^ "_def",
    21.8 +               |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"),
    21.9                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
   21.10             in
   21.11               thy'
   21.12 -             |> PureThy.store_thm (corr_name s vs,
   21.13 +             |> PureThy.store_thm (Binding.name (corr_name s vs),
   21.14                    Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
   21.15                      (Thm.forall_elim_var 0) (forall_intr_frees
   21.16                        (ProofChecker.thm_of_proof thy'
    22.1 --- a/src/Pure/Tools/named_thms.ML	Wed Jan 21 16:47:03 2009 +0100
    22.2 +++ b/src/Pure/Tools/named_thms.ML	Wed Jan 21 16:47:04 2009 +0100
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      Pure/Tools/named_thms.ML
    22.5 -    ID:         $Id$
    22.6      Author:     Makarius
    22.7  
    22.8  Named collections of theorems in canonical order.
    22.9 @@ -36,6 +35,6 @@
   22.10  
   22.11  val setup =
   22.12    Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
   22.13 -  PureThy.add_thms_dynamic (name, Data.get);
   22.14 +  PureThy.add_thms_dynamic (Binding.name name, Data.get);
   22.15  
   22.16  end;
    23.1 --- a/src/Pure/assumption.ML	Wed Jan 21 16:47:03 2009 +0100
    23.2 +++ b/src/Pure/assumption.ML	Wed Jan 21 16:47:04 2009 +0100
    23.3 @@ -1,5 +1,4 @@
    23.4  (*  Title:      Pure/assumption.ML
    23.5 -    ID:         $Id$
    23.6      Author:     Makarius
    23.7  
    23.8  Local assumptions, parameterized by export rules.
    23.9 @@ -79,7 +78,7 @@
   23.10  (* named prems -- legacy feature *)
   23.11  
   23.12  val _ = Context.>>
   23.13 -  (Context.map_theory (PureThy.add_thms_dynamic ("prems",
   23.14 +  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
   23.15      fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
   23.16  
   23.17  
    24.1 --- a/src/Pure/axclass.ML	Wed Jan 21 16:47:03 2009 +0100
    24.2 +++ b/src/Pure/axclass.ML	Wed Jan 21 16:47:04 2009 +0100
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:      Pure/axclass.ML
    24.5 -    ID:         $Id$
    24.6      Author:     Markus Wenzel, TU Muenchen
    24.7  
    24.8  Type classes defined as predicates, associated with a record of
    24.9 @@ -9,7 +8,7 @@
   24.10  signature AX_CLASS =
   24.11  sig
   24.12    val define_class: bstring * class list -> string list ->
   24.13 -    ((Binding.T * attribute list) * term list) list -> theory -> class * theory
   24.14 +    ((binding * attribute list) * term list) list -> theory -> class * theory
   24.15    val add_classrel: thm -> theory -> theory
   24.16    val add_arity: thm -> theory -> theory
   24.17    val prove_classrel: class * class -> tactic -> theory -> theory
   24.18 @@ -329,7 +328,8 @@
   24.19          quote (Syntax.string_of_classrel ctxt [c1, c2]));
   24.20    in
   24.21      thy
   24.22 -    |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])]
   24.23 +    |> PureThy.add_thms [((Binding.name
   24.24 +        (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
   24.25      |-> (fn [th'] => add_classrel th')
   24.26    end;
   24.27  
   24.28 @@ -345,7 +345,7 @@
   24.29            quote (Syntax.string_of_arity ctxt arity));
   24.30    in
   24.31      thy
   24.32 -    |> PureThy.add_thms (map (rpair []) (names ~~ ths))
   24.33 +    |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
   24.34      |-> fold add_arity
   24.35    end;
   24.36  
   24.37 @@ -372,10 +372,10 @@
   24.38      |> Sign.no_base_names
   24.39      |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
   24.40      |-> (fn const' as Const (c'', _) => Thm.add_def false true
   24.41 -          (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
   24.42 +          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
   24.43      #>> Thm.varifyT
   24.44      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
   24.45 -    #> PureThy.add_thm ((c', thm), [Thm.kind_internal])
   24.46 +    #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
   24.47      #> snd
   24.48      #> Sign.restore_naming thy
   24.49      #> pair (Const (c, T))))
   24.50 @@ -391,7 +391,7 @@
   24.51        (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   24.52    in
   24.53      thy
   24.54 -    |> Thm.add_def false false (name', prop)
   24.55 +    |> Thm.add_def false false (Binding.name name', prop)
   24.56      |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   24.57    end;
   24.58  
   24.59 @@ -469,7 +469,7 @@
   24.60      val ([def], def_thy) =
   24.61        thy
   24.62        |> Sign.primitive_class (bclass, super)
   24.63 -      |> PureThy.add_defs false [((Thm.def_name bconst, class_eq), [])];
   24.64 +      |> PureThy.add_defs false [((Binding.name (Thm.def_name bconst), class_eq), [])];
   24.65      val (raw_intro, (raw_classrel, raw_axioms)) =
   24.66        split_defined (length conjs) def ||> chop (length super);
   24.67  
   24.68 @@ -515,7 +515,11 @@
   24.69      val args = prep thy raw_args;
   24.70      val specs = mk args;
   24.71      val names = name args;
   24.72 -  in thy |> PureThy.add_axioms (map (rpair []) (names ~~ specs)) |-> fold add end;
   24.73 +  in
   24.74 +    thy
   24.75 +    |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs))
   24.76 +    |-> fold add
   24.77 +  end;
   24.78  
   24.79  fun ax_classrel prep =
   24.80    axiomatize (map o prep) (map Logic.mk_classrel)
    25.1 --- a/src/Pure/drule.ML	Wed Jan 21 16:47:03 2009 +0100
    25.2 +++ b/src/Pure/drule.ML	Wed Jan 21 16:47:04 2009 +0100
    25.3 @@ -460,10 +460,10 @@
    25.4  val read_prop = certify o SimpleSyntax.read_prop;
    25.5  
    25.6  fun store_thm name th =
    25.7 -  Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
    25.8 +  Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
    25.9  
   25.10  fun store_thm_open name th =
   25.11 -  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
   25.12 +  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (Binding.name name, th)));
   25.13  
   25.14  fun store_standard_thm name th = store_thm name (standard th);
   25.15  fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
    26.1 --- a/src/Pure/more_thm.ML	Wed Jan 21 16:47:03 2009 +0100
    26.2 +++ b/src/Pure/more_thm.ML	Wed Jan 21 16:47:04 2009 +0100
    26.3 @@ -38,8 +38,8 @@
    26.4    val forall_elim_vars: int -> thm -> thm
    26.5    val unvarify: thm -> thm
    26.6    val close_derivation: thm -> thm
    26.7 -  val add_axiom: bstring * term -> theory -> thm * theory
    26.8 -  val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
    26.9 +  val add_axiom: binding * term -> theory -> thm * theory
   26.10 +  val add_def: bool -> bool -> binding * term -> theory -> thm * theory
   26.11    val rule_attribute: (Context.generic -> thm -> thm) -> attribute
   26.12    val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
   26.13    val theory_attributes: attribute list -> theory * thm -> theory * thm
   26.14 @@ -276,14 +276,15 @@
   26.15  
   26.16  (** specification primitives **)
   26.17  
   26.18 -fun add_axiom (name, prop) thy =
   26.19 +fun add_axiom (b, prop) thy =
   26.20    let
   26.21 -    val name' = if name = "" then "axiom_" ^ serial_string () else name;
   26.22 -    val thy' = thy |> Theory.add_axioms_i [(name', prop)];
   26.23 -    val axm = unvarify (Thm.axiom thy' (Sign.full_bname thy' name'));
   26.24 +    val b' = if Binding.is_empty b
   26.25 +      then Binding.name ("axiom_" ^ serial_string ()) else b;
   26.26 +    val thy' = thy |> Theory.add_axioms_i [(b', prop)];
   26.27 +    val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b'));
   26.28    in (axm, thy') end;
   26.29  
   26.30 -fun add_def unchecked overloaded (name, prop) thy =
   26.31 +fun add_def unchecked overloaded (b, prop) thy =
   26.32    let
   26.33      val tfrees = rev (map TFree (Term.add_tfrees prop []));
   26.34      val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
   26.35 @@ -291,8 +292,8 @@
   26.36      val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
   26.37  
   26.38      val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
   26.39 -    val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
   26.40 -    val axm' = Thm.axiom thy' (Sign.full_bname thy' name);
   26.41 +    val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
   26.42 +    val axm' = Thm.axiom thy' (Sign.full_name thy' b);
   26.43      val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
   26.44    in (thm, thy') end;
   26.45  
    27.1 --- a/src/Pure/pure_thy.ML	Wed Jan 21 16:47:03 2009 +0100
    27.2 +++ b/src/Pure/pure_thy.ML	Wed Jan 21 16:47:04 2009 +0100
    27.3 @@ -24,27 +24,27 @@
    27.4    val name_thm: bool -> bool -> Position.T -> string -> thm -> thm
    27.5    val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list
    27.6    val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list
    27.7 -  val store_thms: bstring * thm list -> theory -> thm list * theory
    27.8 -  val store_thm: bstring * thm -> theory -> thm * theory
    27.9 -  val store_thm_open: bstring * thm -> theory -> thm * theory
   27.10 -  val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   27.11 -  val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
   27.12 -  val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
   27.13 -  val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
   27.14 -  val note_thmss: string -> ((Binding.T * attribute list) *
   27.15 +  val store_thms: binding * thm list -> theory -> thm list * theory
   27.16 +  val store_thm: binding * thm -> theory -> thm * theory
   27.17 +  val store_thm_open: binding * thm -> theory -> thm * theory
   27.18 +  val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
   27.19 +  val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   27.20 +  val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
   27.21 +  val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   27.22 +  val note_thmss: string -> ((binding * attribute list) *
   27.23      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
   27.24 -  val note_thmss_grouped: string -> string -> ((Binding.T * attribute list) *
   27.25 +  val note_thmss_grouped: string -> string -> ((binding * attribute list) *
   27.26      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
   27.27 -  val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
   27.28 +  val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   27.29    val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
   27.30 -  val add_defs: bool -> ((bstring * term) * attribute list) list ->
   27.31 +  val add_defs: bool -> ((binding * term) * attribute list) list ->
   27.32      theory -> thm list * theory
   27.33 -  val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list ->
   27.34 +  val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
   27.35 +    theory -> thm list * theory
   27.36 +  val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
   27.37      theory -> thm list * theory
   27.38    val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
   27.39      theory -> thm list * theory
   27.40 -  val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
   27.41 -    theory -> thm list * theory
   27.42    val old_appl_syntax: theory -> bool
   27.43    val old_appl_syntax_setup: theory -> theory
   27.44  end;
   27.45 @@ -163,21 +163,21 @@
   27.46  
   27.47  (* store_thm(s) *)
   27.48  
   27.49 -fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none)
   27.50 -  (name_thms false true Position.none) I (Binding.name bname, thms);
   27.51 +fun store_thms (b, thms) = enter_thms (name_thms true true Position.none)
   27.52 +  (name_thms false true Position.none) I (b, thms);
   27.53  
   27.54 -fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single;
   27.55 +fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
   27.56  
   27.57 -fun store_thm_open (bname, th) =
   27.58 +fun store_thm_open (b, th) =
   27.59    enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
   27.60 -    (Binding.name bname, [th]) #>> the_single;
   27.61 +    (b, [th]) #>> the_single;
   27.62  
   27.63  
   27.64  (* add_thms(s) *)
   27.65  
   27.66 -fun add_thms_atts pre_name ((bname, thms), atts) =
   27.67 +fun add_thms_atts pre_name ((b, thms), atts) =
   27.68    enter_thms pre_name (name_thms false true Position.none)
   27.69 -    (foldl_map (Thm.theory_attributes atts)) (Binding.name bname, thms);
   27.70 +    (foldl_map (Thm.theory_attributes atts)) (b, thms);
   27.71  
   27.72  fun gen_add_thmss pre_name =
   27.73    fold_map (add_thms_atts pre_name);
   27.74 @@ -192,9 +192,9 @@
   27.75  
   27.76  (* add_thms_dynamic *)
   27.77  
   27.78 -fun add_thms_dynamic (bname, f) thy = thy
   27.79 +fun add_thms_dynamic (b, f) thy = thy
   27.80    |> (FactsData.map o apfst)
   27.81 -      (Facts.add_dynamic (Sign.naming_of thy) (Binding.name bname, f) #> snd);
   27.82 +      (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
   27.83  
   27.84  
   27.85  (* note_thmss *)
   27.86 @@ -224,21 +224,21 @@
   27.87  (* store axioms as theorems *)
   27.88  
   27.89  local
   27.90 -  fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_bname thy name);
   27.91 +  fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
   27.92    fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
   27.93 -  fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
   27.94 +  fun add_axm prep_b add = fold_map (fn ((b, ax), atts) => fn thy =>
   27.95      let
   27.96 -      val named_ax = [(name, ax)];
   27.97 +      val named_ax = [(b, ax)];
   27.98        val thy' = add named_ax thy;
   27.99 -      val thm = hd (get_axs thy' named_ax);
  27.100 -    in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end);
  27.101 +      val thm = hd (get_axs thy' ((map o apfst) prep_b named_ax));
  27.102 +    in apfst hd (gen_add_thms (K I) [((prep_b b, thm), atts)] thy') end);
  27.103  in
  27.104 -  val add_defs               = add_axm o Theory.add_defs_i false;
  27.105 -  val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
  27.106 -  val add_axioms             = add_axm Theory.add_axioms_i;
  27.107 -  val add_defs_cmd           = add_axm o Theory.add_defs false;
  27.108 -  val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
  27.109 -  val add_axioms_cmd         = add_axm Theory.add_axioms;
  27.110 +  val add_defs               = add_axm I o Theory.add_defs_i false;
  27.111 +  val add_defs_unchecked     = add_axm I o Theory.add_defs_i true;
  27.112 +  val add_axioms             = add_axm I Theory.add_axioms_i;
  27.113 +  val add_defs_cmd           = add_axm Binding.name o Theory.add_defs false;
  27.114 +  val add_defs_unchecked_cmd = add_axm Binding.name o Theory.add_defs true;
  27.115 +  val add_axioms_cmd         = add_axm Binding.name Theory.add_axioms;
  27.116  end;
  27.117  
  27.118  
  27.119 @@ -378,16 +378,16 @@
  27.120      ("sort_constraint", typ "'a itself => prop", NoSyn),
  27.121      ("conjunction", typ "prop => prop => prop", NoSyn)]
  27.122    #> (add_defs false o map Thm.no_attributes)
  27.123 -   [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
  27.124 -    ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
  27.125 -    ("sort_constraint_def",
  27.126 +   [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
  27.127 +    (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
  27.128 +    (Binding.name "sort_constraint_def",
  27.129        prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
  27.130        \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
  27.131 -    ("conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
  27.132 +    (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
  27.133    #> Sign.hide_const false "Pure.term"
  27.134    #> Sign.hide_const false "Pure.sort_constraint"
  27.135    #> Sign.hide_const false "Pure.conjunction"
  27.136 -  #> add_thmss [(("nothing", []), [])] #> snd
  27.137 -  #> Theory.add_axioms_i Proofterm.equality_axms));
  27.138 +  #> add_thmss [((Binding.name "nothing", []), [])] #> snd
  27.139 +  #> Theory.add_axioms_i ((map o apfst) Binding.name Proofterm.equality_axms)));
  27.140  
  27.141  end;
    28.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Jan 21 16:47:03 2009 +0100
    28.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Jan 21 16:47:04 2009 +0100
    28.3 @@ -247,7 +247,7 @@
    28.4        if need_recursor then
    28.5             thy |> Sign.add_consts_i
    28.6                      [(recursor_base_name, recursor_typ, NoSyn)]
    28.7 -               |> (snd o PureThy.add_defs false [Thm.no_attributes recursor_def])
    28.8 +               |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
    28.9        else thy;
   28.10  
   28.11    val (con_defs, thy0) = thy_path
   28.12 @@ -255,7 +255,7 @@
   28.13                   ((case_base_name, case_typ, NoSyn) ::
   28.14                    map #1 (List.concat con_ty_lists))
   28.15               |> PureThy.add_defs false
   28.16 -                 (map Thm.no_attributes
   28.17 +                 (map (Thm.no_attributes o apfst Binding.name)
   28.18                    (case_def ::
   28.19                     List.concat (ListPair.map mk_con_defs
   28.20                           (1 upto npart, con_ty_lists))))
   28.21 @@ -383,13 +383,13 @@
   28.22    (*Updating theory components: simprules and datatype info*)
   28.23    (thy1 |> Sign.add_path big_rec_base_name
   28.24          |> PureThy.add_thmss
   28.25 -         [(("simps", simps), [Simplifier.simp_add]),
   28.26 -          (("", intrs), [Classical.safe_intro NONE]),
   28.27 -          (("con_defs", con_defs), []),
   28.28 -          (("case_eqns", case_eqns), []),
   28.29 -          (("recursor_eqns", recursor_eqns), []),
   28.30 -          (("free_iffs", free_iffs), []),
   28.31 -          (("free_elims", free_SEs), [])] |> snd
   28.32 +         [((Binding.name "simps", simps), [Simplifier.simp_add]),
   28.33 +          ((Binding.empty , intrs), [Classical.safe_intro NONE]),
   28.34 +          ((Binding.name "con_defs", con_defs), []),
   28.35 +          ((Binding.name "case_eqns", case_eqns), []),
   28.36 +          ((Binding.name "recursor_eqns", recursor_eqns), []),
   28.37 +          ((Binding.name "free_iffs", free_iffs), []),
   28.38 +          ((Binding.name "free_elims", free_SEs), [])] |> snd
   28.39          |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
   28.40          |> ConstructorsData.map (fold Symtab.update con_pairs)
   28.41          |> Sign.parent_path,
    29.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Jan 21 16:47:03 2009 +0100
    29.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Jan 21 16:47:04 2009 +0100
    29.3 @@ -158,7 +158,7 @@
    29.4    in
    29.5      thy
    29.6      |> Sign.add_path (Sign.base_name big_rec_name)
    29.7 -    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
    29.8 +    |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
    29.9      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   29.10      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   29.11      |> Sign.parent_path
    30.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Jan 21 16:47:03 2009 +0100
    30.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Jan 21 16:47:04 2009 +0100
    30.3 @@ -27,10 +27,10 @@
    30.4    (*Insert definitions for the recursive sets, which
    30.5       must *already* be declared as constants in parent theory!*)
    30.6    val add_inductive_i: bool -> term list * term ->
    30.7 -    ((Binding.T * term) * attribute list) list ->
    30.8 +    ((binding * term) * attribute list) list ->
    30.9      thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   30.10    val add_inductive: string list * string ->
   30.11 -    ((Binding.T * string) * Attrib.src list) list ->
   30.12 +    ((binding * string) * Attrib.src list) list ->
   30.13      (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
   30.14      (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
   30.15      theory -> theory * inductive_result
   30.16 @@ -173,7 +173,7 @@
   30.17    val (_, thy1) =
   30.18      thy
   30.19      |> Sign.add_path big_rec_base_name
   30.20 -    |> PureThy.add_defs false (map Thm.no_attributes axpairs);
   30.21 +    |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
   30.22  
   30.23    val ctxt1 = ProofContext.init thy1;
   30.24  
   30.25 @@ -510,9 +510,9 @@
   30.26  
   30.27       val ([induct', mutual_induct'], thy') =
   30.28         thy
   30.29 -       |> PureThy.add_thms [((co_prefix ^ "induct", induct),
   30.30 +       |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
   30.31               [case_names, Induct.induct_pred big_rec_name]),
   30.32 -           (("mutual_induct", mutual_induct), [case_names])];
   30.33 +           ((Binding.name "mutual_induct", mutual_induct), [case_names])];
   30.34      in ((thy', induct'), mutual_induct')
   30.35      end;  (*of induction_rules*)
   30.36  
   30.37 @@ -522,7 +522,7 @@
   30.38      if not coind then induction_rules raw_induct thy1
   30.39      else
   30.40        (thy1
   30.41 -      |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])]
   30.42 +      |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
   30.43        |> apfst hd |> Library.swap, TrueI)
   30.44    and defs = big_rec_def :: part_rec_defs
   30.45  
   30.46 @@ -531,15 +531,15 @@
   30.47      thy2
   30.48      |> IndCases.declare big_rec_name make_cases
   30.49      |> PureThy.add_thms
   30.50 -      [(("bnd_mono", bnd_mono), []),
   30.51 -       (("dom_subset", dom_subset), []),
   30.52 -       (("cases", elim), [case_names, Induct.cases_pred big_rec_name])]
   30.53 +      [((Binding.name "bnd_mono", bnd_mono), []),
   30.54 +       ((Binding.name "dom_subset", dom_subset), []),
   30.55 +       ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
   30.56      ||>> (PureThy.add_thmss o map Thm.no_attributes)
   30.57 -        [("defs", defs),
   30.58 -         ("intros", intrs)];
   30.59 +        [(Binding.name "defs", defs),
   30.60 +         (Binding.name "intros", intrs)];
   30.61    val (intrs'', thy4) =
   30.62      thy3
   30.63 -    |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
   30.64 +    |> PureThy.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
   30.65      ||> Sign.parent_path;
   30.66    in
   30.67      (thy4,
    31.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Jan 21 16:47:03 2009 +0100
    31.2 +++ b/src/ZF/Tools/primrec_package.ML	Wed Jan 21 16:47:04 2009 +0100
    31.3 @@ -8,8 +8,8 @@
    31.4  
    31.5  signature PRIMREC_PACKAGE =
    31.6  sig
    31.7 -  val add_primrec: ((Binding.T * string) * Attrib.src list) list -> theory -> theory * thm list
    31.8 -  val add_primrec_i: ((Binding.T * term) * attribute list) list -> theory -> theory * thm list
    31.9 +  val add_primrec: ((binding * string) * Attrib.src list) list -> theory -> theory * thm list
   31.10 +  val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
   31.11  end;
   31.12  
   31.13  structure PrimrecPackage : PRIMREC_PACKAGE =
   31.14 @@ -169,7 +169,7 @@
   31.15  
   31.16      val ([def_thm], thy1) = thy
   31.17        |> Sign.add_path (Sign.base_name fname)
   31.18 -      |> (PureThy.add_defs false o map Thm.no_attributes) [def];
   31.19 +      |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
   31.20  
   31.21      val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
   31.22      val eqn_thms =
   31.23 @@ -179,10 +179,10 @@
   31.24  
   31.25      val (eqn_thms', thy2) =
   31.26        thy1
   31.27 -      |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts);
   31.28 +      |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
   31.29      val (_, thy3) =
   31.30        thy2
   31.31 -      |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
   31.32 +      |> PureThy.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
   31.33        ||> Sign.parent_path;
   31.34    in (thy3, eqn_thms') end;
   31.35