1.1 --- a/src/CCL/Wfd.thy	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -495,7 +495,7 @@
     1.4  ML {*
     1.5  
     1.6  local
     1.7 -  structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
     1.8 +  structure Data = Named_Thms(val name = @{binding eval} val description = "evaluation rules");
     1.9  in
    1.10  
    1.11  fun eval_tac ths =

     2.1 --- a/src/HOL/Boogie/Boogie.thy	Fri Oct 28 23:16:50 2011 +0200
     2.2 +++ b/src/HOL/Boogie/Boogie.thy	Fri Oct 28 23:41:16 2011 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4  ML {*
     2.5  structure Boogie_Axioms = Named_Thms
     2.6  (
     2.7 -  val name = "boogie"
     2.8 +  val name = @{binding boogie}
     2.9    val description =
    2.10      "Boogie background axioms loaded along with Boogie verification conditions"
    2.11  )

     3.1 --- a/src/HOL/Deriv.thy	Fri Oct 28 23:16:50 2011 +0200
     3.2 +++ b/src/HOL/Deriv.thy	Fri Oct 28 23:41:16 2011 +0200
     3.3 @@ -308,7 +308,7 @@
     3.4  ML {*
     3.5  structure Deriv_Intros = Named_Thms
     3.6  (
     3.7 -  val name = "DERIV_intros"
     3.8 +  val name = @{binding DERIV_intros}
     3.9    val description = "DERIV introduction rules"
    3.10  )
    3.11  *}

     4.1 --- a/src/HOL/Groebner_Basis.thy	Fri Oct 28 23:16:50 2011 +0200
     4.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Oct 28 23:41:16 2011 +0200
     4.3 @@ -32,8 +32,9 @@
     4.4    by auto
     4.5  
     4.6  ML {*
     4.7 -structure Algebra_Simplification = Named_Thms(
     4.8 -  val name = "algebra"
     4.9 +structure Algebra_Simplification = Named_Thms
    4.10 +(
    4.11 +  val name = @{binding algebra}
    4.12    val description = "pre-simplification rules for algebraic methods"
    4.13  )
    4.14  *}

     5.1 --- a/src/HOL/Groups.thy	Fri Oct 28 23:16:50 2011 +0200
     5.2 +++ b/src/HOL/Groups.thy	Fri Oct 28 23:41:16 2011 +0200
     5.3 @@ -12,8 +12,9 @@
     5.4  subsection {* Fact collections *}
     5.5  
     5.6  ML {*
     5.7 -structure Ac_Simps = Named_Thms(
     5.8 -  val name = "ac_simps"
     5.9 +structure Ac_Simps = Named_Thms
    5.10 +(
    5.11 +  val name = @{binding ac_simps}
    5.12    val description = "associativity and commutativity simplification rules"
    5.13  )
    5.14  *}
    5.15 @@ -30,8 +31,9 @@
    5.16  inverses or division. This is catered for by @{text field_simps}. *}
    5.17  
    5.18  ML {*
    5.19 -structure Algebra_Simps = Named_Thms(
    5.20 -  val name = "algebra_simps"
    5.21 +structure Algebra_Simps = Named_Thms
    5.22 +(
    5.23 +  val name = @{binding algebra_simps}
    5.24    val description = "algebra simplification rules"
    5.25  )
    5.26  *}
    5.27 @@ -44,8 +46,9 @@
    5.28  more benign @{text algebra_simps}. *}
    5.29  
    5.30  ML {*
    5.31 -structure Field_Simps = Named_Thms(
    5.32 -  val name = "field_simps"
    5.33 +structure Field_Simps = Named_Thms
    5.34 +(
    5.35 +  val name = @{binding field_simps}
    5.36    val description = "algebra simplification rules for fields"
    5.37  )
    5.38  *}

     6.1 --- a/src/HOL/HOL.thy	Fri Oct 28 23:16:50 2011 +0200
     6.2 +++ b/src/HOL/HOL.thy	Fri Oct 28 23:41:16 2011 +0200
     6.3 @@ -805,7 +805,7 @@
     6.4  ML {*
     6.5  structure No_ATPs = Named_Thms
     6.6  (
     6.7 -  val name = "no_atp"
     6.8 +  val name = @{binding no_atp}
     6.9    val description = "theorems that should be filtered out by Sledgehammer"
    6.10  )
    6.11  *}
    6.12 @@ -1937,22 +1937,22 @@
    6.13  ML {*
    6.14  structure Nitpick_Unfolds = Named_Thms
    6.15  (
    6.16 -  val name = "nitpick_unfold"
    6.17 +  val name = @{binding nitpick_unfold}
    6.18    val description = "alternative definitions of constants as needed by Nitpick"
    6.19  )
    6.20  structure Nitpick_Simps = Named_Thms
    6.21  (
    6.22 -  val name = "nitpick_simp"
    6.23 +  val name = @{binding nitpick_simp}
    6.24    val description = "equational specification of constants as needed by Nitpick"
    6.25  )
    6.26  structure Nitpick_Psimps = Named_Thms
    6.27  (
    6.28 -  val name = "nitpick_psimp"
    6.29 +  val name = @{binding nitpick_psimp}
    6.30    val description = "partial equational specification of constants as needed by Nitpick"
    6.31  )
    6.32  structure Nitpick_Choice_Specs = Named_Thms
    6.33  (
    6.34 -  val name = "nitpick_choice_spec"
    6.35 +  val name = @{binding nitpick_choice_spec}
    6.36    val description = "choice specification of constants as needed by Nitpick"
    6.37  )
    6.38  *}
    6.39 @@ -1973,17 +1973,17 @@
    6.40  ML {*
    6.41  structure Predicate_Compile_Alternative_Defs = Named_Thms
    6.42  (
    6.43 -  val name = "code_pred_def"
    6.44 +  val name = @{binding code_pred_def}
    6.45    val description = "alternative definitions of constants for the Predicate Compiler"
    6.46  )
    6.47  structure Predicate_Compile_Inline_Defs = Named_Thms
    6.48  (
    6.49 -  val name = "code_pred_inline"
    6.50 +  val name = @{binding code_pred_inline}
    6.51    val description = "inlining definitions for the Predicate Compiler"
    6.52  )
    6.53  structure Predicate_Compile_Simps = Named_Thms
    6.54  (
    6.55 -  val name = "code_pred_simp"
    6.56 +  val name = @{binding code_pred_simp}
    6.57    val description = "simplification rules for the optimisations in the Predicate Compiler"
    6.58  )
    6.59  *}

     7.1 --- a/src/HOL/HOLCF/Cont.thy	Fri Oct 28 23:16:50 2011 +0200
     7.2 +++ b/src/HOL/HOLCF/Cont.thy	Fri Oct 28 23:41:16 2011 +0200
     7.3 @@ -123,7 +123,7 @@
     7.4  ML {*
     7.5  structure Cont2ContData = Named_Thms
     7.6  (
     7.7 -  val name = "cont2cont"
     7.8 +  val name = @{binding cont2cont}
     7.9    val description = "continuity intro rule"
    7.10  )
    7.11  *}

     8.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Oct 28 23:16:50 2011 +0200
     8.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Oct 28 23:41:16 2011 +0200
     8.3 @@ -46,13 +46,13 @@
     8.4  
     8.5  structure RepData = Named_Thms
     8.6  (
     8.7 -  val name = "domain_defl_simps"
     8.8 +  val name = @{binding domain_defl_simps}
     8.9    val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
    8.10  )
    8.11  
    8.12  structure IsodeflData = Named_Thms
    8.13  (
    8.14 -  val name = "domain_isodefl"
    8.15 +  val name = @{binding domain_isodefl}
    8.16    val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
    8.17  )
    8.18  

     9.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Oct 28 23:16:50 2011 +0200
     9.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Oct 28 23:41:16 2011 +0200
     9.3 @@ -125,13 +125,13 @@
     9.4  
     9.5  structure DeflMapData = Named_Thms
     9.6  (
     9.7 -  val name = "domain_deflation"
     9.8 +  val name = @{binding domain_deflation}
     9.9    val description = "theorems like deflation a ==> deflation (foo_map$a)"
    9.10  )
    9.11  
    9.12  structure Map_Id_Data = Named_Thms
    9.13  (
    9.14 -  val name = "domain_map_ID"
    9.15 +  val name = @{binding domain_map_ID}
    9.16    val description = "theorems like foo_map$ID = ID"
    9.17  )
    9.18  

    10.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 28 23:16:50 2011 +0200
    10.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 28 23:41:16 2011 +0200
    10.3 @@ -40,8 +40,9 @@
    10.4    "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
    10.5      by (cases f, cases g) (auto simp: fun_eq_iff)
    10.6  
    10.7 -ML {* structure Execute_Simps = Named_Thms(
    10.8 -  val name = "execute_simps"
    10.9 +ML {* structure Execute_Simps = Named_Thms
   10.10 +(
   10.11 +  val name = @{binding execute_simps}
   10.12    val description = "simplification rules for execute"
   10.13  ) *}
   10.14  
   10.15 @@ -93,8 +94,9 @@
   10.16      and "execute f h \<noteq> None"
   10.17    using assms by (simp add: success_def)
   10.18  
   10.19 -ML {* structure Success_Intros = Named_Thms(
   10.20 -  val name = "success_intros"
   10.21 +ML {* structure Success_Intros = Named_Thms
   10.22 +(
   10.23 +  val name = @{binding success_intros}
   10.24    val description = "introduction rules for success"
   10.25  ) *}
   10.26  
   10.27 @@ -166,13 +168,15 @@
   10.28    shows "a = b" and "h' = h''"
   10.29    using assms unfolding effect_def by auto
   10.30  
   10.31 -ML {* structure Crel_Intros = Named_Thms(
   10.32 -  val name = "effect_intros"
   10.33 +ML {* structure Crel_Intros = Named_Thms
   10.34 +(
   10.35 +  val name = @{binding effect_intros}
   10.36    val description = "introduction rules for effect"
   10.37  ) *}
   10.38  
   10.39 -ML {* structure Crel_Elims = Named_Thms(
   10.40 -  val name = "effect_elims"
   10.41 +ML {* structure Crel_Elims = Named_Thms
   10.42 +(
   10.43 +  val name = @{binding effect_elims}
   10.44    val description = "elimination rules for effect"
   10.45  ) *}
   10.46  

    11.1 --- a/src/HOL/Limits.thy	Fri Oct 28 23:16:50 2011 +0200
    11.2 +++ b/src/HOL/Limits.thy	Fri Oct 28 23:41:16 2011 +0200
    11.3 @@ -540,7 +540,7 @@
    11.4  ML {*
    11.5  structure Tendsto_Intros = Named_Thms
    11.6  (
    11.7 -  val name = "tendsto_intros"
    11.8 +  val name = @{binding tendsto_intros}
    11.9    val description = "introduction rules for tendsto"
   11.10  )
   11.11  *}

    12.1 --- a/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 23:16:50 2011 +0200
    12.2 +++ b/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 23:41:16 2011 +0200
    12.3 @@ -161,7 +161,7 @@
    12.4  
    12.5  structure Termination_Simps = Named_Thms
    12.6  (
    12.7 -  val name = "termination_simp"
    12.8 +  val name = @{binding termination_simp}
    12.9    val description = "simplification rules for termination proofs"
   12.10  )
   12.11  

    13.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Fri Oct 28 23:16:50 2011 +0200
    13.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Oct 28 23:41:16 2011 +0200
    13.3 @@ -18,7 +18,7 @@
    13.4  (** User-declared size functions **)
    13.5  structure Measure_Heuristic_Rules = Named_Thms
    13.6  (
    13.7 -  val name = "measure_function"
    13.8 +  val name = @{binding measure_function}
    13.9    val description =
   13.10      "rules that guide the heuristic generation of measure functions"
   13.11  );

    14.1 --- a/src/HOL/Tools/Function/partial_function.ML	Fri Oct 28 23:16:50 2011 +0200
    14.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Fri Oct 28 23:41:16 2011 +0200
    14.3 @@ -53,7 +53,7 @@
    14.4  
    14.5  structure Mono_Rules = Named_Thms
    14.6  (
    14.7 -  val name = "partial_function_mono";
    14.8 +  val name = @{binding partial_function_mono};
    14.9    val description = "monotonicity rules for partial function definitions";
   14.10  );
   14.11  

    15.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Oct 28 23:16:50 2011 +0200
    15.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Oct 28 23:41:16 2011 +0200
    15.3 @@ -184,7 +184,7 @@
    15.4  (* equivalence relation theorems *)
    15.5  structure Equiv_Rules = Named_Thms
    15.6  (
    15.7 -  val name = "quot_equiv"
    15.8 +  val name = @{binding quot_equiv}
    15.9    val description = "equivalence relation theorems"
   15.10  )
   15.11  
   15.12 @@ -194,7 +194,7 @@
   15.13  (* respectfulness theorems *)
   15.14  structure Rsp_Rules = Named_Thms
   15.15  (
   15.16 -  val name = "quot_respect"
   15.17 +  val name = @{binding quot_respect}
   15.18    val description = "respectfulness theorems"
   15.19  )
   15.20  
   15.21 @@ -204,7 +204,7 @@
   15.22  (* preservation theorems *)
   15.23  structure Prs_Rules = Named_Thms
   15.24  (
   15.25 -  val name = "quot_preserve"
   15.26 +  val name = @{binding quot_preserve}
   15.27    val description = "preservation theorems"
   15.28  )
   15.29  
   15.30 @@ -214,7 +214,7 @@
   15.31  (* id simplification theorems *)
   15.32  structure Id_Simps = Named_Thms
   15.33  (
   15.34 -  val name = "id_simps"
   15.35 +  val name = @{binding id_simps}
   15.36    val description = "identity simp rules for maps"
   15.37  )
   15.38  
   15.39 @@ -223,7 +223,7 @@
   15.40  (* quotient theorems *)
   15.41  structure Quotient_Rules = Named_Thms
   15.42  (
   15.43 -  val name = "quot_thm"
   15.44 +  val name = @{binding quot_thm}
   15.45    val description = "quotient theorems"
   15.46  )
   15.47  

    16.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Oct 28 23:16:50 2011 +0200
    16.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Oct 28 23:41:16 2011 +0200
    16.3 @@ -672,7 +672,7 @@
    16.4       * ... ? **)
    16.5  structure Z3_Simps = Named_Thms
    16.6  (
    16.7 -  val name = "z3_simp"
    16.8 +  val name = @{binding z3_simp}
    16.9    val description = "simplification rules for Z3 proof reconstruction"
   16.10  )
   16.11  

    17.1 --- a/src/HOL/Tools/arith_data.ML	Fri Oct 28 23:16:50 2011 +0200
    17.2 +++ b/src/HOL/Tools/arith_data.ML	Fri Oct 28 23:41:16 2011 +0200
    17.3 @@ -32,8 +32,8 @@
    17.4  
    17.5  structure Arith_Facts = Named_Thms
    17.6  (
    17.7 -  val name = "arith"
    17.8 -  val description = "arith facts - only ground formulas"
    17.9 +  val name = @{binding arith}
   17.10 +  val description = "arith facts -- only ground formulas"
   17.11  );
   17.12  
   17.13  val get_arith_facts = Arith_Facts.get;

    18.1 --- a/src/HOL/ex/Numeral.thy	Fri Oct 28 23:16:50 2011 +0200
    18.2 +++ b/src/HOL/ex/Numeral.thy	Fri Oct 28 23:41:16 2011 +0200
    18.3 @@ -96,7 +96,7 @@
    18.4  ML {*
    18.5  structure Dig_Simps = Named_Thms
    18.6  (
    18.7 -  val name = "numeral"
    18.8 +  val name = @{binding numeral}
    18.9    val description = "simplification rules for numerals"
   18.10  )
   18.11  *}

    19.1 --- a/src/Pure/Tools/named_thms.ML	Fri Oct 28 23:16:50 2011 +0200
    19.2 +++ b/src/Pure/Tools/named_thms.ML	Fri Oct 28 23:41:16 2011 +0200
    19.3 @@ -15,7 +15,7 @@
    19.4    val setup: theory -> theory
    19.5  end;
    19.6  
    19.7 -functor Named_Thms(val name: string val description: string): NAMED_THMS =
    19.8 +functor Named_Thms(val name: binding val description: string): NAMED_THMS =
    19.9  struct
   19.10  
   19.11  structure Data = Generic_Data
   19.12 @@ -38,7 +38,7 @@
   19.13  val del = Thm.declaration_attribute del_thm;
   19.14  
   19.15  val setup =
   19.16 -  Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
   19.17 -  Global_Theory.add_thms_dynamic (Binding.name name, content);
   19.18 +  Attrib.setup name (Attrib.add_del add del) ("declaration of " ^ description) #>
   19.19 +  Global_Theory.add_thms_dynamic (name, content);
   19.20  
   19.21  end;

    20.1 --- a/src/Tools/atomize_elim.ML	Fri Oct 28 23:16:50 2011 +0200
    20.2 +++ b/src/Tools/atomize_elim.ML	Fri Oct 28 23:41:16 2011 +0200
    20.3 @@ -23,7 +23,7 @@
    20.4  
    20.5  structure AtomizeElimData = Named_Thms
    20.6  (
    20.7 -  val name = "atomize_elim";
    20.8 +  val name = @{binding atomize_elim};
    20.9    val description = "atomize_elim rewrite rule";
   20.10  );
   20.11  

    21.1 --- a/src/ZF/UNITY/Constrains.thy	Fri Oct 28 23:16:50 2011 +0200
    21.2 +++ b/src/ZF/UNITY/Constrains.thy	Fri Oct 28 23:41:16 2011 +0200
    21.3 @@ -464,7 +464,7 @@
    21.4  (*To allow expansion of the program's definition when appropriate*)
    21.5  structure Program_Defs = Named_Thms
    21.6  (
    21.7 -  val name = "program"
    21.8 +  val name = @{binding program}
    21.9    val description = "program definitions"
   21.10  );
   21.11