# HG changeset patch
# User wenzelm
# Date 1319838076 -7200
# Node ID 3c5d3d28605558e4d35db40e2c075c68a07bd278
# Parent  57def0b396965ea646453a98959423c3b79c8876
tuned Named_Thms: proper binding;

diff -r 57def0b39696 -r 3c5d3d286055 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/CCL/Wfd.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -495,7 +495,7 @@
 ML {*
 
 local
-  structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
+  structure Data = Named_Thms(val name = @{binding eval} val description = "evaluation rules");
 in
 
 fun eval_tac ths =
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Boogie/Boogie.thy
--- a/src/HOL/Boogie/Boogie.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Boogie/Boogie.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -86,7 +86,7 @@
 ML {*
 structure Boogie_Axioms = Named_Thms
 (
-  val name = "boogie"
+  val name = @{binding boogie}
   val description =
     "Boogie background axioms loaded along with Boogie verification conditions"
 )
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Deriv.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -308,7 +308,7 @@
 ML {*
 structure Deriv_Intros = Named_Thms
 (
-  val name = "DERIV_intros"
+  val name = @{binding DERIV_intros}
   val description = "DERIV introduction rules"
 )
 *}
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Groebner_Basis.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -32,8 +32,9 @@
   by auto
 
 ML {*
-structure Algebra_Simplification = Named_Thms(
-  val name = "algebra"
+structure Algebra_Simplification = Named_Thms
+(
+  val name = @{binding algebra}
   val description = "pre-simplification rules for algebraic methods"
 )
 *}
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Groups.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -12,8 +12,9 @@
 subsection {* Fact collections *}
 
 ML {*
-structure Ac_Simps = Named_Thms(
-  val name = "ac_simps"
+structure Ac_Simps = Named_Thms
+(
+  val name = @{binding ac_simps}
   val description = "associativity and commutativity simplification rules"
 )
 *}
@@ -30,8 +31,9 @@
 inverses or division. This is catered for by @{text field_simps}. *}
 
 ML {*
-structure Algebra_Simps = Named_Thms(
-  val name = "algebra_simps"
+structure Algebra_Simps = Named_Thms
+(
+  val name = @{binding algebra_simps}
   val description = "algebra simplification rules"
 )
 *}
@@ -44,8 +46,9 @@
 more benign @{text algebra_simps}. *}
 
 ML {*
-structure Field_Simps = Named_Thms(
-  val name = "field_simps"
+structure Field_Simps = Named_Thms
+(
+  val name = @{binding field_simps}
   val description = "algebra simplification rules for fields"
 )
 *}
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -805,7 +805,7 @@
 ML {*
 structure No_ATPs = Named_Thms
 (
-  val name = "no_atp"
+  val name = @{binding no_atp}
   val description = "theorems that should be filtered out by Sledgehammer"
 )
 *}
@@ -1937,22 +1937,22 @@
 ML {*
 structure Nitpick_Unfolds = Named_Thms
 (
-  val name = "nitpick_unfold"
+  val name = @{binding nitpick_unfold}
   val description = "alternative definitions of constants as needed by Nitpick"
 )
 structure Nitpick_Simps = Named_Thms
 (
-  val name = "nitpick_simp"
+  val name = @{binding nitpick_simp}
   val description = "equational specification of constants as needed by Nitpick"
 )
 structure Nitpick_Psimps = Named_Thms
 (
-  val name = "nitpick_psimp"
+  val name = @{binding nitpick_psimp}
   val description = "partial equational specification of constants as needed by Nitpick"
 )
 structure Nitpick_Choice_Specs = Named_Thms
 (
-  val name = "nitpick_choice_spec"
+  val name = @{binding nitpick_choice_spec}
   val description = "choice specification of constants as needed by Nitpick"
 )
 *}
@@ -1973,17 +1973,17 @@
 ML {*
 structure Predicate_Compile_Alternative_Defs = Named_Thms
 (
-  val name = "code_pred_def"
+  val name = @{binding code_pred_def}
   val description = "alternative definitions of constants for the Predicate Compiler"
 )
 structure Predicate_Compile_Inline_Defs = Named_Thms
 (
-  val name = "code_pred_inline"
+  val name = @{binding code_pred_inline}
   val description = "inlining definitions for the Predicate Compiler"
 )
 structure Predicate_Compile_Simps = Named_Thms
 (
-  val name = "code_pred_simp"
+  val name = @{binding code_pred_simp}
   val description = "simplification rules for the optimisations in the Predicate Compiler"
 )
 *}
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/HOLCF/Cont.thy
--- a/src/HOL/HOLCF/Cont.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/HOLCF/Cont.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -123,7 +123,7 @@
 ML {*
 structure Cont2ContData = Named_Thms
 (
-  val name = "cont2cont"
+  val name = @{binding cont2cont}
   val description = "continuity intro rule"
 )
 *}
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -46,13 +46,13 @@
 
 structure RepData = Named_Thms
 (
-  val name = "domain_defl_simps"
+  val name = @{binding domain_defl_simps}
   val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
 )
 
 structure IsodeflData = Named_Thms
 (
-  val name = "domain_isodefl"
+  val name = @{binding domain_isodefl}
   val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
 )
 
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -125,13 +125,13 @@
 
 structure DeflMapData = Named_Thms
 (
-  val name = "domain_deflation"
+  val name = @{binding domain_deflation}
   val description = "theorems like deflation a ==> deflation (foo_map$a)"
 )
 
 structure Map_Id_Data = Named_Thms
 (
-  val name = "domain_map_ID"
+  val name = @{binding domain_map_ID}
   val description = "theorems like foo_map$ID = ID"
 )
 
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -40,8 +40,9 @@
   "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
     by (cases f, cases g) (auto simp: fun_eq_iff)
 
-ML {* structure Execute_Simps = Named_Thms(
-  val name = "execute_simps"
+ML {* structure Execute_Simps = Named_Thms
+(
+  val name = @{binding execute_simps}
   val description = "simplification rules for execute"
 ) *}
 
@@ -93,8 +94,9 @@
     and "execute f h \<noteq> None"
   using assms by (simp add: success_def)
 
-ML {* structure Success_Intros = Named_Thms(
-  val name = "success_intros"
+ML {* structure Success_Intros = Named_Thms
+(
+  val name = @{binding success_intros}
   val description = "introduction rules for success"
 ) *}
 
@@ -166,13 +168,15 @@
   shows "a = b" and "h' = h''"
   using assms unfolding effect_def by auto
 
-ML {* structure Crel_Intros = Named_Thms(
-  val name = "effect_intros"
+ML {* structure Crel_Intros = Named_Thms
+(
+  val name = @{binding effect_intros}
   val description = "introduction rules for effect"
 ) *}
 
-ML {* structure Crel_Elims = Named_Thms(
-  val name = "effect_elims"
+ML {* structure Crel_Elims = Named_Thms
+(
+  val name = @{binding effect_elims}
   val description = "elimination rules for effect"
 ) *}
 
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Limits.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -540,7 +540,7 @@
 ML {*
 structure Tendsto_Intros = Named_Thms
 (
-  val name = "tendsto_intros"
+  val name = @{binding tendsto_intros}
   val description = "introduction rules for tendsto"
 )
 *}
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -161,7 +161,7 @@
 
 structure Termination_Simps = Named_Thms
 (
-  val name = "termination_simp"
+  val name = @{binding termination_simp}
   val description = "simplification rules for termination proofs"
 )
 
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Tools/Function/measure_functions.ML
--- a/src/HOL/Tools/Function/measure_functions.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -18,7 +18,7 @@
 (** User-declared size functions **)
 structure Measure_Heuristic_Rules = Named_Thms
 (
-  val name = "measure_function"
+  val name = @{binding measure_function}
   val description =
     "rules that guide the heuristic generation of measure functions"
 );
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -53,7 +53,7 @@
 
 structure Mono_Rules = Named_Thms
 (
-  val name = "partial_function_mono";
+  val name = @{binding partial_function_mono};
   val description = "monotonicity rules for partial function definitions";
 );
 
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -184,7 +184,7 @@
 (* equivalence relation theorems *)
 structure Equiv_Rules = Named_Thms
 (
-  val name = "quot_equiv"
+  val name = @{binding quot_equiv}
   val description = "equivalence relation theorems"
 )
 
@@ -194,7 +194,7 @@
 (* respectfulness theorems *)
 structure Rsp_Rules = Named_Thms
 (
-  val name = "quot_respect"
+  val name = @{binding quot_respect}
   val description = "respectfulness theorems"
 )
 
@@ -204,7 +204,7 @@
 (* preservation theorems *)
 structure Prs_Rules = Named_Thms
 (
-  val name = "quot_preserve"
+  val name = @{binding quot_preserve}
   val description = "preservation theorems"
 )
 
@@ -214,7 +214,7 @@
 (* id simplification theorems *)
 structure Id_Simps = Named_Thms
 (
-  val name = "id_simps"
+  val name = @{binding id_simps}
   val description = "identity simp rules for maps"
 )
 
@@ -223,7 +223,7 @@
 (* quotient theorems *)
 structure Quotient_Rules = Named_Thms
 (
-  val name = "quot_thm"
+  val name = @{binding quot_thm}
   val description = "quotient theorems"
 )
 
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -672,7 +672,7 @@
      * ... ? **)
 structure Z3_Simps = Named_Thms
 (
-  val name = "z3_simp"
+  val name = @{binding z3_simp}
   val description = "simplification rules for Z3 proof reconstruction"
 )
 
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Tools/arith_data.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -32,8 +32,8 @@
 
 structure Arith_Facts = Named_Thms
 (
-  val name = "arith"
-  val description = "arith facts - only ground formulas"
+  val name = @{binding arith}
+  val description = "arith facts -- only ground formulas"
 );
 
 val get_arith_facts = Arith_Facts.get;
diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/ex/Numeral.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -96,7 +96,7 @@
 ML {*
 structure Dig_Simps = Named_Thms
 (
-  val name = "numeral"
+  val name = @{binding numeral}
   val description = "simplification rules for numerals"
 )
 *}
diff -r 57def0b39696 -r 3c5d3d286055 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/Pure/Tools/named_thms.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -15,7 +15,7 @@
   val setup: theory -> theory
 end;
 
-functor Named_Thms(val name: string val description: string): NAMED_THMS =
+functor Named_Thms(val name: binding val description: string): NAMED_THMS =
 struct
 
 structure Data = Generic_Data
@@ -38,7 +38,7 @@
 val del = Thm.declaration_attribute del_thm;
 
 val setup =
-  Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
-  Global_Theory.add_thms_dynamic (Binding.name name, content);
+  Attrib.setup name (Attrib.add_del add del) ("declaration of " ^ description) #>
+  Global_Theory.add_thms_dynamic (name, content);
 
 end;
diff -r 57def0b39696 -r 3c5d3d286055 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/Tools/atomize_elim.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -23,7 +23,7 @@
 
 structure AtomizeElimData = Named_Thms
 (
-  val name = "atomize_elim";
+  val name = @{binding atomize_elim};
   val description = "atomize_elim rewrite rule";
 );
 
diff -r 57def0b39696 -r 3c5d3d286055 src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/ZF/UNITY/Constrains.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -464,7 +464,7 @@
 (*To allow expansion of the program's definition when appropriate*)
 structure Program_Defs = Named_Thms
 (
-  val name = "program"
+  val name = @{binding program}
   val description = "program definitions"
 );