# HG changeset patch
# User haftmann
# Date 1232552824 -3600
# Node ID cb520b766e0086fb5679ffd2489c45d1b219ccf0
# Parent  8c4e961fcb08f0ded511f9edd15a90c19b9ac49f
binding replaces bstring

diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -390,7 +390,7 @@
                           (wfrec $ map_types poly_tvars R)
                       $ functional
      val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
-     val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy
+     val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
  in (thy', def) end;
 end;
 
@@ -549,7 +549,7 @@
      val ([def0], theory) =
        thy
        |> PureThy.add_defs false
-            [Thm.no_attributes (fid ^ "_def", defn)]
+            [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
      val def = Thm.freezeT def0;
      val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
                            else ()
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -238,7 +238,7 @@
           (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
       |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
-          ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
+          (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
@@ -262,7 +262,7 @@
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
-    |> PureThy.add_thmss [(("recs", rec_thms), [])]
+    |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [])]
     ||> Sign.parent_path
     ||> Theory.checkpoint
     |-> (fn thms => pair (reccomb_names, Library.flat thms))
@@ -316,7 +316,7 @@
             fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
           val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
           val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn);
-          val def = ((Sign.base_name name) ^ "_def",
+          val def = (Binding.name (Sign.base_name name ^ "_def"),
             Logic.mk_equals (list_comb (Const (name, caseT), fns1),
               list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
                 fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -76,7 +76,7 @@
 fun store_thmss_atts label tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
     Sign.add_path tname
-    #> PureThy.add_thmss [((label, thms), atts)]
+    #> PureThy.add_thmss [((Binding.name label, thms), atts)]
     #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
@@ -85,7 +85,7 @@
 fun store_thms_atts label tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
     Sign.add_path tname
-    #> PureThy.add_thms [((label, thms), atts)]
+    #> PureThy.add_thms [((Binding.name label, thms), atts)]
     #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -196,13 +196,13 @@
 
 fun add_rules simps case_thms rec_thms inject distinct
                   weak_case_congs cong_att =
-  PureThy.add_thmss [(("simps", simps), []),
-    (("", flat case_thms @
+  PureThy.add_thmss [((Binding.name "simps", simps), []),
+    ((Binding.empty, flat case_thms @
           flat distinct @ rec_thms), [Simplifier.simp_add]),
-    (("", rec_thms), [Code.add_default_eqn_attribute]),
-    (("", flat inject), [iff_add]),
-    (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
-    (("", weak_case_congs), [cong_att])]
+    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
+    ((Binding.empty, flat inject), [iff_add]),
+    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
+    ((Binding.empty, weak_case_congs), [cong_att])]
   #> snd;
 
 
@@ -213,15 +213,15 @@
     val inducts = ProjectRule.projections (ProofContext.init thy) induction;
 
     fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
-      [(("", nth inducts index), [Induct.induct_type name]),
-       (("", exhaustion), [Induct.cases_type name])];
+      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
+       ((Binding.empty, exhaustion), [Induct.cases_type name])];
     fun unnamed_rule i =
-      (("", nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
+      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
   in
     thy |> PureThy.add_thms
       (maps named_rules infos @
         map unnamed_rule (length infos upto length inducts - 1)) |> snd
-    |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd
+    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
   end;
 
 
@@ -451,7 +451,7 @@
       |> store_thmss "inject" new_type_names inject
       ||>> store_thmss "distinct" new_type_names distinct
       ||> Sign.add_path (space_implode "_" new_type_names)
-      ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])];
+      ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
 
     val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
       ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -130,7 +130,7 @@
     val vs = map (fn i => List.nth (pnames, i)) is;
     val (thm', thy') = thy
       |> Sign.absolute_path
-      |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm)
+      |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
       ||> Sign.restore_naming thy;
 
     val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
@@ -196,7 +196,7 @@
     val exh_name = Thm.get_name exhaustion;
     val (thm', thy') = thy
       |> Sign.absolute_path
-      |> PureThy.store_thm (exh_name ^ "_P_correctness", thm)
+      |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm)
       ||> Sign.restore_naming thy;
 
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -242,7 +242,7 @@
         val ([def_thm], thy') =
           thy
           |> Sign.add_consts_i [(cname', constrT, mx)]
-          |> (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)];
+          |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
 
       in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
 
@@ -343,7 +343,7 @@
         
         val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
         val fTs = map fastype_of fs;
-        val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
+        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Sign.base_name iso_name ^ "_def"),
           Logic.mk_equals (Const (iso_name, T --> Univ_elT),
             list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
         val (def_thms, thy') =
@@ -631,7 +631,7 @@
     val ([dt_induct'], thy7) =
       thy6
       |> Sign.add_path big_name
-      |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
+      |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
       ||> Sign.parent_path
       ||> Theory.checkpoint;
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -144,7 +144,7 @@
            (size_names ~~ recTs1))
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
-           (def_names ~~ (size_fns ~~ rec_combs1)))
+           (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
       ||> TheoryTarget.instantiation
            (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
       ||>> fold_map define_overloaded
@@ -208,7 +208,7 @@
       prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
 
     val ([size_thms], thy'') =  PureThy.add_thmss
-      [(("size", size_eqns),
+      [((Binding.name "size", size_eqns),
         [Simplifier.simp_add, Thm.declaration_attribute
               (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -391,14 +391,14 @@
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
              [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
-        val (thm', thy') = PureThy.store_thm (space_implode "_"
-          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
+        val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
+          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
           (DatatypeAux.split_conj_thm thm');
         val ([thms'], thy'') = PureThy.add_thmss
-          [((space_implode "_"
+          [((Binding.name (space_implode "_"
              (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
-               ["correctness"]), thms), [])] thy';
+               ["correctness"])), thms), [])] thy';
         val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
       in
         Extraction.add_realizers_i
@@ -451,8 +451,8 @@
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
-        val (thm', thy') = PureThy.store_thm (space_implode "_"
-          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
+        val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
+          (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
       in
         Extraction.add_realizers_i
           [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/old_primrec_package.ML
--- a/src/HOL/Tools/old_primrec_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -305,11 +305,11 @@
   end;
 
 fun thy_note ((name, atts), thms) =
-  PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
+  PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
 fun thy_def false ((name, atts), t) =
-      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+      PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
   | thy_def true ((name, atts), t) =
-      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+      PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
 
 in
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/recdef_package.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Wrapper module for Konrad Slind's TFL package.
@@ -16,10 +15,10 @@
   val cong_del: attribute
   val wf_add: attribute
   val wf_del: attribute
-  val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
+  val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
     Attrib.src option -> theory -> theory
       * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
-  val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
+  val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
     theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
     -> theory -> theory * {induct_rules: thm}
@@ -214,8 +213,8 @@
       thy
       |> Sign.add_path bname
       |> PureThy.add_thmss
-        ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
-      ||>> PureThy.add_thms [(("induct", induct), [])];
+        (((Binding.name "simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
+      ||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
       thy
@@ -243,7 +242,7 @@
     val ([induct_rules'], thy3) =
       thy2
       |> Sign.add_path bname
-      |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
+      |> PureThy.add_thms [((Binding.name "induct_rules", induct_rules), [])]
       ||> Sign.parent_path;
   in (thy3, {induct_rules = induct_rules'}) end;
 
@@ -299,7 +298,7 @@
 
 val recdef_decl =
   Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
-  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
+  P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
     -- Scan.option hints
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -1534,8 +1534,10 @@
       |> extension_typedef name repT (alphas@[zeta])
       ||> Sign.add_consts_i
             (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
-      ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
-      ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
+      ||>> PureThy.add_defs false
+            (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
+      ||>> PureThy.add_defs false
+            (map (Thm.no_attributes o apfst Binding.name) upd_specs)
       |-> (fn args as ((_, dest_defs), upd_defs) =>
           fold Code.add_default_eqn dest_defs
           #> fold Code.add_default_eqn upd_defs
@@ -1693,14 +1695,14 @@
           [dest_convs',upd_convs']),
       thm_thy) =
       defs_thy
-      |> (PureThy.add_thms o map Thm.no_attributes)
+      |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
            [("ext_inject", inject),
             ("ext_induct", induct),
             ("ext_cases", cases),
             ("ext_surjective", surjective),
             ("ext_split", split_meta)]
-      ||>> (PureThy.add_thmss o map Thm.no_attributes)
-              [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)]
+      ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
+            [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)]
 
   in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
   end;
@@ -1938,9 +1940,9 @@
           (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
       |> (Sign.add_consts_i o map Syntax.no_syn)
           (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
-      |> ((PureThy.add_defs false o map Thm.no_attributes) sel_specs)
-      ||>> ((PureThy.add_defs false o map Thm.no_attributes) upd_specs)
-      ||>> ((PureThy.add_defs false o map Thm.no_attributes)
+      |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
+      ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
+      ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
              [make_spec, fields_spec, extend_spec, truncate_spec])
       |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
           fold Code.add_default_eqn sel_defs
@@ -2164,17 +2166,17 @@
     val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'],
             [surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) =
       defs_thy
-      |> (PureThy.add_thmss o map Thm.no_attributes)
+      |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
          [("select_convs", sel_convs_standard),
           ("update_convs", upd_convs),
           ("select_defs", sel_defs),
           ("update_defs", upd_defs),
           ("splits", [split_meta_standard,split_object,split_ex]),
           ("defs", derived_defs)]
-      ||>> (PureThy.add_thms o map Thm.no_attributes)
+      ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
           [("surjective", surjective),
            ("equality", equality)]
-      ||>> PureThy.add_thms
+      ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name)
         [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
          (("induct", induct), induct_type_global name),
          (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
@@ -2186,8 +2188,8 @@
     val final_thy =
       thms_thy
       |> (snd oo PureThy.add_thmss)
-          [(("simps", sel_upd_simps), [Simplifier.simp_add]),
-           (("iffs",iffs), [iff_add])]
+          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
+           ((Binding.name "iffs", iffs), [iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme')
       |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
       |> add_record_equalities extension_id equality'
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -84,7 +84,7 @@
             val (c, thy') =
               Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy
             val cdef = cname ^ "_def"
-            val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
+            val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
             val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
           in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
       | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -28,7 +28,7 @@
                                else thname
                 val def_eq = Logic.mk_equals (Const(cname_full,ctype),
                                               HOLogic.choice_const ctype $  P)
-                val (thms, thy') = PureThy.add_defs covld [((cdefname,def_eq),[])] thy
+                val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
                 val thm' = [thm,hd thms] MRS @{thm exE_some}
             in
                 mk_definitional cos (thy',thm')
@@ -39,7 +39,7 @@
         let
             fun process [] (thy,tm) =
                 let
-                    val (thms, thy') = PureThy.add_axioms [((axname,HOLogic.mk_Trueprop tm),[])] thy
+                    val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy
                 in
                     (thy',hd thms)
                 end
@@ -184,7 +184,7 @@
                             if name = ""
                             then arg |> Library.swap
                             else (writeln ("  " ^ name ^ ": " ^ (Display.string_of_thm thm));
-                                  PureThy.store_thm (name, thm) thy)
+                                  PureThy.store_thm (Binding.name name, thm) thy)
                     in
                         args |> apsnd (remove_alls frees)
                              |> apsnd undo_imps
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -112,7 +112,8 @@
       if def then
         theory
         |> Sign.add_consts_i [(name, setT', NoSyn)]
-        |> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))]
+        |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
+            (PrimitiveDefs.mk_defpair (setC, set)))]
         |-> (fn [th] => pair (SOME th))
       else (NONE, theory);
     fun contract_def NONE th = th
@@ -130,7 +131,7 @@
          (Abs_name, oldT --> newT, NoSyn)]
       #> add_def
       #-> (fn set_def =>
-        PureThy.add_axioms [((typedef_name, typedef_prop),
+        PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
           [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
         ##>> pair set_def)
       ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
@@ -143,7 +144,7 @@
             thy1
             |> Sign.add_path name
             |> PureThy.add_thms
-              ([((Rep_name, make @{thm type_definition.Rep}), []),
+              ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []),
                 ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
                 ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
                 ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
diff -r 8c4e961fcb08 -r cb520b766e00 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/ex/Quickcheck.thy	Wed Jan 21 16:47:04 2009 +0100
@@ -200,7 +200,7 @@
             in
               lthy
               |> LocalTheory.theory (Code.del_eqns c
-                   #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
+                   #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal])
                    #-> Code.add_eqn)
             end;
         in
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/calculation.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -98,8 +98,8 @@
     ("sym", sym_att, "declaration of symmetry rule"),
     ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
   PureThy.add_thms
-   [(("", transitive_thm), [trans_add]),
-    (("", symmetric_thm), [sym_add])] #> snd));
+   [((Binding.empty, transitive_thm), [trans_add]),
+    ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
 
 
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -8,12 +8,12 @@
 
 signature CONSTDEFS =
 sig
-  val add_constdefs: (Binding.T * string option) list *
-    ((Binding.T * string option * mixfix) option *
+  val add_constdefs: (binding * string option) list *
+    ((binding * string option * mixfix) option *
       (Attrib.binding * string)) list -> theory -> theory
-  val add_constdefs_i: (Binding.T * typ option) list *
-    ((Binding.T * typ option * mixfix) option *
-      ((Binding.T * attribute list) * term)) list -> theory -> theory
+  val add_constdefs_i: (binding * typ option) list *
+    ((binding * typ option * mixfix) option *
+      ((binding * attribute list) * term)) list -> theory -> theory
 end;
 
 structure Constdefs: CONSTDEFS =
@@ -52,7 +52,7 @@
     val thy' =
       thy
       |> Sign.add_consts_i [(c, T, mx)]
-      |> PureThy.add_defs false [((name, def), atts)]
+      |> PureThy.add_defs false [((Binding.name name, def), atts)]
       |-> (fn [thm] => Code.add_default_eqn thm);
   in ((c, T), thy') end;
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -13,8 +13,8 @@
   val typed_print_translation: bool * (string * Position.T) -> theory -> theory
   val print_ast_translation: bool * (string * Position.T) -> theory -> theory
   val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
-  val add_axioms: ((Binding.T * string) * Attrib.src list) list -> theory -> theory
-  val add_defs: (bool * bool) * ((Binding.T * string) * Attrib.src list) list -> theory -> theory
+  val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
+  val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
   val declaration: string * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> string * Position.T -> string list ->
     local_theory -> local_theory
@@ -53,7 +53,6 @@
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
-  val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_simpset: Toplevel.transition -> Toplevel.transition
   val print_rules: Toplevel.transition -> Toplevel.transition
@@ -359,12 +358,6 @@
   Toplevel.keep (fn state =>
     Locale.print_locale (Toplevel.theory_of state) show_facts name);
 
-fun print_registrations show_wits name = Toplevel.unknown_context o
-  Toplevel.keep (Toplevel.node_case
-      (Context.cases (Old_Locale.print_registrations show_wits name o ProofContext.init)
-        (Old_Locale.print_registrations show_wits name))
-    (Old_Locale.print_registrations show_wits name o Proof.context_of));
-
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/overloading.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -134,8 +134,8 @@
 
 fun declare c_ty = pair (Const c_ty);
 
-fun define checked name (c, t) =
-  Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t));
+fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name,
+  Logic.mk_equals (Const (c, Term.fastype_of t), t));
 
 
 (* target *)
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -126,7 +126,8 @@
 
 fun ml_store sel (name, ths) =
   let
-    val ths' = Context.>>> (Context.map_theory_result (PureThy.store_thms (name, ths)));
+    val ths' = Context.>>> (Context.map_theory_result
+      (PureThy.store_thms (Binding.name name, ths)));
     val _ =
       if name = "" then ()
       else if not (ML_Syntax.is_identifier name) then
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -733,11 +733,11 @@
              val (def_thms, thy') = if t = nullt then ([], thy) else
                thy
                |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
-               |> PureThy.add_defs false [((extr_name s vs ^ "_def",
+               |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"),
                     Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
            in
              thy'
-             |> PureThy.store_thm (corr_name s vs,
+             |> PureThy.store_thm (Binding.name (corr_name s vs),
                   Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
                     (Thm.forall_elim_var 0) (forall_intr_frees
                       (ProofChecker.thm_of_proof thy'
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Tools/named_thms.ML
-    ID:         $Id$
     Author:     Makarius
 
 Named collections of theorems in canonical order.
@@ -36,6 +35,6 @@
 
 val setup =
   Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
-  PureThy.add_thms_dynamic (name, Data.get);
+  PureThy.add_thms_dynamic (Binding.name name, Data.get);
 
 end;
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/assumption.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/assumption.ML
-    ID:         $Id$
     Author:     Makarius
 
 Local assumptions, parameterized by export rules.
@@ -79,7 +78,7 @@
 (* named prems -- legacy feature *)
 
 val _ = Context.>>
-  (Context.map_theory (PureThy.add_thms_dynamic ("prems",
+  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
     fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
 
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/axclass.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/axclass.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Type classes defined as predicates, associated with a record of
@@ -9,7 +8,7 @@
 signature AX_CLASS =
 sig
   val define_class: bstring * class list -> string list ->
-    ((Binding.T * attribute list) * term list) list -> theory -> class * theory
+    ((binding * attribute list) * term list) list -> theory -> class * theory
   val add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
   val prove_classrel: class * class -> tactic -> theory -> theory
@@ -329,7 +328,8 @@
         quote (Syntax.string_of_classrel ctxt [c1, c2]));
   in
     thy
-    |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])]
+    |> PureThy.add_thms [((Binding.name
+        (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
     |-> (fn [th'] => add_classrel th')
   end;
 
@@ -345,7 +345,7 @@
           quote (Syntax.string_of_arity ctxt arity));
   in
     thy
-    |> PureThy.add_thms (map (rpair []) (names ~~ ths))
+    |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
     |-> fold add_arity
   end;
 
@@ -372,10 +372,10 @@
     |> Sign.no_base_names
     |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
     |-> (fn const' as Const (c'', _) => Thm.add_def false true
-          (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
+          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
     #>> Thm.varifyT
     #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
-    #> PureThy.add_thm ((c', thm), [Thm.kind_internal])
+    #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
     #> snd
     #> Sign.restore_naming thy
     #> pair (Const (c, T))))
@@ -391,7 +391,7 @@
       (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   in
     thy
-    |> Thm.add_def false false (name', prop)
+    |> Thm.add_def false false (Binding.name name', prop)
     |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   end;
 
@@ -469,7 +469,7 @@
     val ([def], def_thy) =
       thy
       |> Sign.primitive_class (bclass, super)
-      |> PureThy.add_defs false [((Thm.def_name bconst, class_eq), [])];
+      |> PureThy.add_defs false [((Binding.name (Thm.def_name bconst), class_eq), [])];
     val (raw_intro, (raw_classrel, raw_axioms)) =
       split_defined (length conjs) def ||> chop (length super);
 
@@ -515,7 +515,11 @@
     val args = prep thy raw_args;
     val specs = mk args;
     val names = name args;
-  in thy |> PureThy.add_axioms (map (rpair []) (names ~~ specs)) |-> fold add end;
+  in
+    thy
+    |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs))
+    |-> fold add
+  end;
 
 fun ax_classrel prep =
   axiomatize (map o prep) (map Logic.mk_classrel)
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/drule.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -460,10 +460,10 @@
 val read_prop = certify o SimpleSyntax.read_prop;
 
 fun store_thm name th =
-  Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
+  Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
 
 fun store_thm_open name th =
-  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
+  Context.>>> (Context.map_theory_result (PureThy.store_thm_open (Binding.name name, th)));
 
 fun store_standard_thm name th = store_thm name (standard th);
 fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/more_thm.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -38,8 +38,8 @@
   val forall_elim_vars: int -> thm -> thm
   val unvarify: thm -> thm
   val close_derivation: thm -> thm
-  val add_axiom: bstring * term -> theory -> thm * theory
-  val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
+  val add_axiom: binding * term -> theory -> thm * theory
+  val add_def: bool -> bool -> binding * term -> theory -> thm * theory
   val rule_attribute: (Context.generic -> thm -> thm) -> attribute
   val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
   val theory_attributes: attribute list -> theory * thm -> theory * thm
@@ -276,14 +276,15 @@
 
 (** specification primitives **)
 
-fun add_axiom (name, prop) thy =
+fun add_axiom (b, prop) thy =
   let
-    val name' = if name = "" then "axiom_" ^ serial_string () else name;
-    val thy' = thy |> Theory.add_axioms_i [(name', prop)];
-    val axm = unvarify (Thm.axiom thy' (Sign.full_bname thy' name'));
+    val b' = if Binding.is_empty b
+      then Binding.name ("axiom_" ^ serial_string ()) else b;
+    val thy' = thy |> Theory.add_axioms_i [(b', prop)];
+    val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b'));
   in (axm, thy') end;
 
-fun add_def unchecked overloaded (name, prop) thy =
+fun add_def unchecked overloaded (b, prop) thy =
   let
     val tfrees = rev (map TFree (Term.add_tfrees prop []));
     val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
@@ -291,8 +292,8 @@
     val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
 
     val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
-    val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
-    val axm' = Thm.axiom thy' (Sign.full_bname thy' name);
+    val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
+    val axm' = Thm.axiom thy' (Sign.full_name thy' b);
     val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
   in (thm, thy') end;
 
diff -r 8c4e961fcb08 -r cb520b766e00 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/pure_thy.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -24,27 +24,27 @@
   val name_thm: bool -> bool -> Position.T -> string -> thm -> thm
   val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list
   val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list
-  val store_thms: bstring * thm list -> theory -> thm list * theory
-  val store_thm: bstring * thm -> theory -> thm * theory
-  val store_thm_open: bstring * thm -> theory -> thm * theory
-  val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
-  val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
-  val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
-  val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
-  val note_thmss: string -> ((Binding.T * attribute list) *
+  val store_thms: binding * thm list -> theory -> thm list * theory
+  val store_thm: binding * thm -> theory -> thm * theory
+  val store_thm_open: binding * thm -> theory -> thm * theory
+  val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
+  val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
+  val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
+  val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
+  val note_thmss: string -> ((binding * attribute list) *
     (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
-  val note_thmss_grouped: string -> string -> ((Binding.T * attribute list) *
+  val note_thmss_grouped: string -> string -> ((binding * attribute list) *
     (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
-  val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
+  val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
-  val add_defs: bool -> ((bstring * term) * attribute list) list ->
+  val add_defs: bool -> ((binding * term) * attribute list) list ->
     theory -> thm list * theory
-  val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list ->
+  val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
+    theory -> thm list * theory
+  val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
     theory -> thm list * theory
   val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
     theory -> thm list * theory
-  val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
-    theory -> thm list * theory
   val old_appl_syntax: theory -> bool
   val old_appl_syntax_setup: theory -> theory
 end;
@@ -163,21 +163,21 @@
 
 (* store_thm(s) *)
 
-fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none)
-  (name_thms false true Position.none) I (Binding.name bname, thms);
+fun store_thms (b, thms) = enter_thms (name_thms true true Position.none)
+  (name_thms false true Position.none) I (b, thms);
 
-fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single;
+fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
 
-fun store_thm_open (bname, th) =
+fun store_thm_open (b, th) =
   enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
-    (Binding.name bname, [th]) #>> the_single;
+    (b, [th]) #>> the_single;
 
 
 (* add_thms(s) *)
 
-fun add_thms_atts pre_name ((bname, thms), atts) =
+fun add_thms_atts pre_name ((b, thms), atts) =
   enter_thms pre_name (name_thms false true Position.none)
-    (foldl_map (Thm.theory_attributes atts)) (Binding.name bname, thms);
+    (foldl_map (Thm.theory_attributes atts)) (b, thms);
 
 fun gen_add_thmss pre_name =
   fold_map (add_thms_atts pre_name);
@@ -192,9 +192,9 @@
 
 (* add_thms_dynamic *)
 
-fun add_thms_dynamic (bname, f) thy = thy
+fun add_thms_dynamic (b, f) thy = thy
   |> (FactsData.map o apfst)
-      (Facts.add_dynamic (Sign.naming_of thy) (Binding.name bname, f) #> snd);
+      (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
 
 
 (* note_thmss *)
@@ -224,21 +224,21 @@
 (* store axioms as theorems *)
 
 local
-  fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_bname thy name);
+  fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
   fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
-  fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
+  fun add_axm prep_b add = fold_map (fn ((b, ax), atts) => fn thy =>
     let
-      val named_ax = [(name, ax)];
+      val named_ax = [(b, ax)];
       val thy' = add named_ax thy;
-      val thm = hd (get_axs thy' named_ax);
-    in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end);
+      val thm = hd (get_axs thy' ((map o apfst) prep_b named_ax));
+    in apfst hd (gen_add_thms (K I) [((prep_b b, thm), atts)] thy') end);
 in
-  val add_defs               = add_axm o Theory.add_defs_i false;
-  val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
-  val add_axioms             = add_axm Theory.add_axioms_i;
-  val add_defs_cmd           = add_axm o Theory.add_defs false;
-  val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
-  val add_axioms_cmd         = add_axm Theory.add_axioms;
+  val add_defs               = add_axm I o Theory.add_defs_i false;
+  val add_defs_unchecked     = add_axm I o Theory.add_defs_i true;
+  val add_axioms             = add_axm I Theory.add_axioms_i;
+  val add_defs_cmd           = add_axm Binding.name o Theory.add_defs false;
+  val add_defs_unchecked_cmd = add_axm Binding.name o Theory.add_defs true;
+  val add_axioms_cmd         = add_axm Binding.name Theory.add_axioms;
 end;
 
 
@@ -378,16 +378,16 @@
     ("sort_constraint", typ "'a itself => prop", NoSyn),
     ("conjunction", typ "prop => prop => prop", NoSyn)]
   #> (add_defs false o map Thm.no_attributes)
-   [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
-    ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
-    ("sort_constraint_def",
+   [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
+    (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
+    (Binding.name "sort_constraint_def",
       prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
       \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
-    ("conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
+    (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
   #> Sign.hide_const false "Pure.term"
   #> Sign.hide_const false "Pure.sort_constraint"
   #> Sign.hide_const false "Pure.conjunction"
-  #> add_thmss [(("nothing", []), [])] #> snd
-  #> Theory.add_axioms_i Proofterm.equality_axms));
+  #> add_thmss [((Binding.name "nothing", []), [])] #> snd
+  #> Theory.add_axioms_i ((map o apfst) Binding.name Proofterm.equality_axms)));
 
 end;
diff -r 8c4e961fcb08 -r cb520b766e00 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -247,7 +247,7 @@
       if need_recursor then
            thy |> Sign.add_consts_i
                     [(recursor_base_name, recursor_typ, NoSyn)]
-               |> (snd o PureThy.add_defs false [Thm.no_attributes recursor_def])
+               |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
       else thy;
 
   val (con_defs, thy0) = thy_path
@@ -255,7 +255,7 @@
                  ((case_base_name, case_typ, NoSyn) ::
                   map #1 (List.concat con_ty_lists))
              |> PureThy.add_defs false
-                 (map Thm.no_attributes
+                 (map (Thm.no_attributes o apfst Binding.name)
                   (case_def ::
                    List.concat (ListPair.map mk_con_defs
                          (1 upto npart, con_ty_lists))))
@@ -383,13 +383,13 @@
   (*Updating theory components: simprules and datatype info*)
   (thy1 |> Sign.add_path big_rec_base_name
         |> PureThy.add_thmss
-         [(("simps", simps), [Simplifier.simp_add]),
-          (("", intrs), [Classical.safe_intro NONE]),
-          (("con_defs", con_defs), []),
-          (("case_eqns", case_eqns), []),
-          (("recursor_eqns", recursor_eqns), []),
-          (("free_iffs", free_iffs), []),
-          (("free_elims", free_SEs), [])] |> snd
+         [((Binding.name "simps", simps), [Simplifier.simp_add]),
+          ((Binding.empty , intrs), [Classical.safe_intro NONE]),
+          ((Binding.name "con_defs", con_defs), []),
+          ((Binding.name "case_eqns", case_eqns), []),
+          ((Binding.name "recursor_eqns", recursor_eqns), []),
+          ((Binding.name "free_iffs", free_iffs), []),
+          ((Binding.name "free_elims", free_SEs), [])] |> snd
         |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
         |> ConstructorsData.map (fold Symtab.update con_pairs)
         |> Sign.parent_path,
diff -r 8c4e961fcb08 -r cb520b766e00 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -158,7 +158,7 @@
   in
     thy
     |> Sign.add_path (Sign.base_name big_rec_name)
-    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
+    |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
     |> Sign.parent_path
diff -r 8c4e961fcb08 -r cb520b766e00 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -27,10 +27,10 @@
   (*Insert definitions for the recursive sets, which
      must *already* be declared as constants in parent theory!*)
   val add_inductive_i: bool -> term list * term ->
-    ((Binding.T * term) * attribute list) list ->
+    ((binding * term) * attribute list) list ->
     thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   val add_inductive: string list * string ->
-    ((Binding.T * string) * Attrib.src list) list ->
+    ((binding * string) * Attrib.src list) list ->
     (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
     (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
     theory -> theory * inductive_result
@@ -173,7 +173,7 @@
   val (_, thy1) =
     thy
     |> Sign.add_path big_rec_base_name
-    |> PureThy.add_defs false (map Thm.no_attributes axpairs);
+    |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
 
   val ctxt1 = ProofContext.init thy1;
 
@@ -510,9 +510,9 @@
 
      val ([induct', mutual_induct'], thy') =
        thy
-       |> PureThy.add_thms [((co_prefix ^ "induct", induct),
+       |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
              [case_names, Induct.induct_pred big_rec_name]),
-           (("mutual_induct", mutual_induct), [case_names])];
+           ((Binding.name "mutual_induct", mutual_induct), [case_names])];
     in ((thy', induct'), mutual_induct')
     end;  (*of induction_rules*)
 
@@ -522,7 +522,7 @@
     if not coind then induction_rules raw_induct thy1
     else
       (thy1
-      |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])]
+      |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
       |> apfst hd |> Library.swap, TrueI)
   and defs = big_rec_def :: part_rec_defs
 
@@ -531,15 +531,15 @@
     thy2
     |> IndCases.declare big_rec_name make_cases
     |> PureThy.add_thms
-      [(("bnd_mono", bnd_mono), []),
-       (("dom_subset", dom_subset), []),
-       (("cases", elim), [case_names, Induct.cases_pred big_rec_name])]
+      [((Binding.name "bnd_mono", bnd_mono), []),
+       ((Binding.name "dom_subset", dom_subset), []),
+       ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
     ||>> (PureThy.add_thmss o map Thm.no_attributes)
-        [("defs", defs),
-         ("intros", intrs)];
+        [(Binding.name "defs", defs),
+         (Binding.name "intros", intrs)];
   val (intrs'', thy4) =
     thy3
-    |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
+    |> PureThy.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
     ||> Sign.parent_path;
   in
     (thy4,
diff -r 8c4e961fcb08 -r cb520b766e00 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -8,8 +8,8 @@
 
 signature PRIMREC_PACKAGE =
 sig
-  val add_primrec: ((Binding.T * string) * Attrib.src list) list -> theory -> theory * thm list
-  val add_primrec_i: ((Binding.T * term) * attribute list) list -> theory -> theory * thm list
+  val add_primrec: ((binding * string) * Attrib.src list) list -> theory -> theory * thm list
+  val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -169,7 +169,7 @@
 
     val ([def_thm], thy1) = thy
       |> Sign.add_path (Sign.base_name fname)
-      |> (PureThy.add_defs false o map Thm.no_attributes) [def];
+      |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
 
     val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
     val eqn_thms =
@@ -179,10 +179,10 @@
 
     val (eqn_thms', thy2) =
       thy1
-      |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts);
+      |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
     val (_, thy3) =
       thy2
-      |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
+      |> PureThy.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
       ||> Sign.parent_path;
   in (thy3, eqn_thms') end;