prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;

--- a/src/CCL/Wfd.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/CCL/Wfd.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -483,15 +483,14 @@
 
 subsection {* Evaluation *}
 
+named_theorems eval "evaluation rules"
+
 ML {*
-structure Eval_Rules =
-  Named_Thms(val name = @{binding eval} val description = "evaluation rules");
-
 fun eval_tac ths =
-  Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
-    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Eval_Rules.get context) 1));
+  Subgoal.FOCUS_PREMS (fn {context = ctxt, prems, ...} =>
+    let val eval_rules = Named_Theorems.get ctxt @{named_theorems eval}
+    in DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ rev eval_rules) 1) end)
 *}
-setup Eval_Rules.setup
 
 method_setup eval = {*
   Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))

--- a/src/Cube/Cube.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/Cube/Cube.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -10,14 +10,7 @@
 
 setup Pure_Thy.old_appl_syntax_setup
 
-ML {*
-  structure Rules = Named_Thms
-  (
-    val name = @{binding rules}
-    val description = "Cube inference rules"
-  )
-*}
-setup Rules.setup
+named_theorems rules "Cube inference rules"
 
 typedecl "term"
 typedecl "context"

--- a/src/HOL/HOLCF/Cfun.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -147,7 +147,7 @@
       val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
       val tr = instantiate' [SOME T, SOME U] [SOME f]
           (mk_meta_eq @{thm Abs_cfun_inverse2});
-      val rules = Cont2ContData.get ctxt;
+      val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
       val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
     in SOME (perhaps (SINGLE (tac 1)) tr) end
 *}

--- a/src/HOL/HOLCF/Cont.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Cont.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -120,15 +120,8 @@
 
 subsection {* Collection of continuity rules *}
 
-ML {*
-structure Cont2ContData = Named_Thms
-(
-  val name = @{binding cont2cont}
-  val description = "continuity intro rule"
-)
-*}
+named_theorems cont2cont "continuity intro rule"
 
-setup Cont2ContData.setup
 
 subsection {* Continuity of basic functions *}
 

--- a/src/HOL/HOLCF/Domain.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Domain.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -316,12 +316,13 @@
 
 subsection {* Setting up the domain package *}
 
+named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
+named_theorems domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
+
 ML_file "Tools/Domain/domain_isomorphism.ML"
 ML_file "Tools/Domain/domain_axioms.ML"
 ML_file "Tools/Domain/domain.ML"
 
-setup Domain_Isomorphism.setup
-
 lemmas [domain_defl_simps] =
   DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
   liftdefl_eq LIFTDEFL_prod u_liftdefl_liftdefl_of

--- a/src/HOL/HOLCF/Domain_Aux.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -344,6 +344,9 @@
 
 subsection {* ML setup *}
 
+named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
+named_theorems domain_map_ID "theorems like foo_map$ID = ID"
+
 ML_file "Tools/Domain/domain_take_proofs.ML"
 ML_file "Tools/cont_consts.ML"
 ML_file "Tools/cont_proc.ML"

--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 11:35:33 2014 +0200
@@ -28,8 +28,6 @@
   val domain_isomorphism_cmd :
     (string list * binding * mixfix * string * (binding * binding) option) list
       -> theory -> theory
-
-  val setup : theory -> theory
 end
 
 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
@@ -41,24 +39,6 @@
 
 fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
 
-(******************************************************************************)
-(******************************** theory data *********************************)
-(******************************************************************************)
-
-structure RepData = Named_Thms
-(
-  val name = @{binding domain_defl_simps}
-  val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
-)
-
-structure IsodeflData = Named_Thms
-(
-  val name = @{binding domain_isodefl}
-  val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
-)
-
-val setup = RepData.setup #> IsodeflData.setup
-
 
 (******************************************************************************)
 (************************** building types and terms **************************)
@@ -170,7 +150,7 @@
     val cont_thm =
       let
         val prop = mk_trp (mk_cont functional)
-        val rules = Cont2ContData.get (Proof_Context.init_global thy)
+        val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
         val tac = REPEAT_ALL_NEW (match_tac rules) 1
       in
         Goal.prove_global thy [] [] prop (K tac)
@@ -207,7 +187,8 @@
     (tab2 : (typ * term) list)
     (T : typ) : term =
   let
-    val defl_simps = RepData.get (Proof_Context.init_global thy)
+    val defl_simps =
+      Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
     val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps
     val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2
     fun proc1 t =
@@ -522,7 +503,8 @@
         val ((_, _, _, {DEFL, ...}), thy) =
           Domaindef.add_domaindef spec defl NONE thy
         (* declare domain_defl_simps rules *)
-        val thy = Context.theory_map (RepData.add_thm DEFL) thy
+        val thy =
+          Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_defl_simps} DEFL) thy
       in
         (DEFL, thy)
       end
@@ -532,7 +514,8 @@
     fun mk_DEFL_eq_thm (lhsT, rhsT) =
       let
         val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
-        val DEFL_simps = RepData.get (Proof_Context.init_global thy)
+        val DEFL_simps =
+          Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
         fun tac ctxt =
           rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
           THEN TRY (resolve_tac defl_unfold_thms 1)
@@ -637,7 +620,7 @@
         val isodefl_rules =
           @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
           @ isodefl_abs_rep_thms
-          @ IsodeflData.get (Proof_Context.init_global thy)
+          @ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl}
       in
         Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
          EVERY
@@ -661,7 +644,9 @@
     val (isodefl_thms, thy) = thy |>
       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
         (conjuncts isodefl_binds isodefl_thm)
-    val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy
+    val thy =
+      fold (Context.theory_map o Named_Theorems.add_thm @{named_theorems domain_isodefl})
+        isodefl_thms thy
 
     (* prove map_ID theorems *)
     fun prove_map_ID_thm

--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Aug 16 11:35:33 2014 +0200
@@ -123,31 +123,20 @@
   fun merge data = Symtab.merge (K true) data
 )
 
-structure DeflMapData = Named_Thms
-(
-  val name = @{binding domain_deflation}
-  val description = "theorems like deflation a ==> deflation (foo_map$a)"
-)
-
-structure Map_Id_Data = Named_Thms
-(
-  val name = @{binding domain_map_ID}
-  val description = "theorems like foo_map$ID = ID"
-)
-
 fun add_rec_type (tname, bs) =
     Rec_Data.map (Symtab.insert (K true) (tname, bs))
 
 fun add_deflation_thm thm =
-    Context.theory_map (DeflMapData.add_thm thm)
+    Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm)
 
 val get_rec_tab = Rec_Data.get
-fun get_deflation_thms thy = DeflMapData.get (Proof_Context.init_global thy)
+fun get_deflation_thms thy =
+  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation}
 
-val map_ID_add = Map_Id_Data.add
-val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global
+val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID}
+fun get_map_ID_thms thy =
+  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID}
 
-val _ = Theory.setup (DeflMapData.setup #> Map_Id_Data.setup)
 
 (******************************************************************************)
 (************************** building types and terms **************************)

--- a/src/HOL/HOLCF/Tools/fixrec.ML	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Aug 16 11:35:33 2014 +0200
@@ -130,7 +130,7 @@
           "or simp rules are configured for all non-HOLCF constants.\n" ^
           "The error occurred for the goal statement:\n" ^
           Syntax.string_of_term lthy prop)
-        val rules = Cont2ContData.get lthy
+        val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
         val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules))
         val slow_tac = SOLVED' (simp_tac lthy)
         val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err

--- a/src/ZF/UNITY/Constrains.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/ZF/UNITY/Constrains.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -453,6 +453,9 @@
   used by Always_Int_I) *)
 lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
 
+(*To allow expansion of the program's definition when appropriate*)
+named_theorems program "program definitions"
+
 ML
 {*
 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
@@ -461,13 +464,6 @@
 (*Combines a list of invariance THEOREMS into one.*)
 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
 
-(*To allow expansion of the program's definition when appropriate*)
-structure Program_Defs = Named_Thms
-(
-  val name = @{binding program}
-  val description = "program definitions"
-);
-
 (*proves "co" properties when the program is specified*)
 
 fun constrains_tac ctxt =
@@ -481,7 +477,7 @@
               (* Three subgoals *)
               rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
               REPEAT (force_tac ctxt 2),
-              full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1,
+              full_simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 1,
               ALLGOALS (clarify_tac ctxt),
               REPEAT (FIRSTGOAL (etac @{thm disjE})),
               ALLGOALS (clarify_tac ctxt),
@@ -495,8 +491,6 @@
     rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
 *}
 
-setup Program_Defs.setup
-
 method_setup safety = {*
   Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
   "for proving safety properties"

--- a/src/ZF/UNITY/SubstAx.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/ZF/UNITY/SubstAx.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -358,7 +358,7 @@
                 REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
                                   @{thm EnsuresI}, @{thm ensuresI}] 1),
             (*now there are two subgoals: co & transient*)
-            simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 2,
+            simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,
             res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
                (*simplify the command's domain*)
             simp_tac (ctxt addsimps [@{thm domain_def}]) 3,