renamed NamedThmsFun to Named_Thms;
authorwenzelm
Thu Jul 02 17:34:14 2009 +0200 (2009-07-02)
changeset 31902862ae16a799d
parent 31901 e280491f36b8
child 31903 c5221dbc40f6
renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
src/CCL/Wfd.thy
src/HOL/Deriv.thy
src/HOL/HOL.thy
src/HOL/Limits.thy
src/HOL/Nominal/nominal_primrec.ML
src/HOL/OrderedGroup.thy
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Function/fundef.ML
src/HOL/Tools/Function/fundef_common.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/measure_functions.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.ML
src/HOL/ex/Numeral.thy
src/HOLCF/Cont.thy
src/Tools/atomize_elim.ML
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/CCL/Wfd.thy	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -495,7 +495,7 @@
     1.4  ML {*
     1.5  
     1.6  local
     1.7 -  structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules");
     1.8 +  structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
     1.9  in
    1.10  
    1.11  fun eval_tac ctxt ths =
     2.1 --- a/src/HOL/Deriv.thy	Thu Jul 02 17:33:36 2009 +0200
     2.2 +++ b/src/HOL/Deriv.thy	Thu Jul 02 17:34:14 2009 +0200
     2.3 @@ -315,14 +315,14 @@
     2.4  
     2.5  text {* @{text "DERIV_intros"} *}
     2.6  ML {*
     2.7 -structure DerivIntros = NamedThmsFun
     2.8 +structure Deriv_Intros = Named_Thms
     2.9  (
    2.10    val name = "DERIV_intros"
    2.11    val description = "DERIV introduction rules"
    2.12  )
    2.13  *}
    2.14  
    2.15 -setup DerivIntros.setup
    2.16 +setup Deriv_Intros.setup
    2.17  
    2.18  lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
    2.19    by simp
     3.1 --- a/src/HOL/HOL.thy	Thu Jul 02 17:33:36 2009 +0200
     3.2 +++ b/src/HOL/HOL.thy	Thu Jul 02 17:34:14 2009 +0200
     3.3 @@ -923,9 +923,11 @@
     3.4  ML_Antiquote.value "claset"
     3.5    (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())");
     3.6  
     3.7 -structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
     3.8 +structure ResAtpset = Named_Thms
     3.9 +  (val name = "atp" val description = "ATP rules");
    3.10  
    3.11 -structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP");
    3.12 +structure ResBlacklist = Named_Thms
    3.13 +  (val name = "noatp" val description = "theorems blacklisted for ATP");
    3.14  *}
    3.15  
    3.16  text {*ResBlacklist holds theorems blacklisted to sledgehammer. 
    3.17 @@ -1982,19 +1984,18 @@
    3.18    Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
    3.19  *} "solve goal by normalization"
    3.20  
    3.21 +
    3.22  subsubsection {* Quickcheck *}
    3.23  
    3.24  ML {*
    3.25 -structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun
    3.26 +structure Quickcheck_RecFun_Simps = Named_Thms
    3.27  (
    3.28    val name = "quickcheck_recfun_simp"
    3.29    val description = "simplification rules of recursive functions as needed by Quickcheck"
    3.30  )
    3.31  *}
    3.32  
    3.33 -setup {*
    3.34 -  Quickcheck_RecFun_Simp_Thms.setup
    3.35 -*}
    3.36 +setup Quickcheck_RecFun_Simps.setup
    3.37  
    3.38  setup {*
    3.39    Quickcheck.add_generator ("SML", Codegen.test_term)
    3.40 @@ -2008,22 +2009,22 @@
    3.41  text {* This will be relocated once Nitpick is moved to HOL. *}
    3.42  
    3.43  ML {*
    3.44 -structure Nitpick_Const_Def_Thms = NamedThmsFun
    3.45 +structure Nitpick_Const_Defs = Named_Thms
    3.46  (
    3.47    val name = "nitpick_const_def"
    3.48    val description = "alternative definitions of constants as needed by Nitpick"
    3.49  )
    3.50 -structure Nitpick_Const_Simp_Thms = NamedThmsFun
    3.51 +structure Nitpick_Const_Simps = Named_Thms
    3.52  (
    3.53    val name = "nitpick_const_simp"
    3.54    val description = "equational specification of constants as needed by Nitpick"
    3.55  )
    3.56 -structure Nitpick_Const_Psimp_Thms = NamedThmsFun
    3.57 +structure Nitpick_Const_Psimps = Named_Thms
    3.58  (
    3.59    val name = "nitpick_const_psimp"
    3.60    val description = "partial equational specification of constants as needed by Nitpick"
    3.61  )
    3.62 -structure Nitpick_Ind_Intro_Thms = NamedThmsFun
    3.63 +structure Nitpick_Ind_Intros = Named_Thms
    3.64  (
    3.65    val name = "nitpick_ind_intro"
    3.66    val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    3.67 @@ -2031,10 +2032,10 @@
    3.68  *}
    3.69  
    3.70  setup {*
    3.71 -  Nitpick_Const_Def_Thms.setup
    3.72 -  #> Nitpick_Const_Simp_Thms.setup
    3.73 -  #> Nitpick_Const_Psimp_Thms.setup
    3.74 -  #> Nitpick_Ind_Intro_Thms.setup
    3.75 +  Nitpick_Const_Defs.setup
    3.76 +  #> Nitpick_Const_Simps.setup
    3.77 +  #> Nitpick_Const_Psimps.setup
    3.78 +  #> Nitpick_Ind_Intros.setup
    3.79  *}
    3.80  
    3.81  
     4.1 --- a/src/HOL/Limits.thy	Thu Jul 02 17:33:36 2009 +0200
     4.2 +++ b/src/HOL/Limits.thy	Thu Jul 02 17:34:14 2009 +0200
     4.3 @@ -350,7 +350,7 @@
     4.4  lemmas Zfun_mult_left = mult.Zfun_left
     4.5  
     4.6  
     4.7 -subsection{* Limits *}
     4.8 +subsection {* Limits *}
     4.9  
    4.10  definition
    4.11    tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
    4.12 @@ -358,13 +358,15 @@
    4.13  where [code del]:
    4.14    "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
    4.15  
    4.16 -ML{*
    4.17 -structure TendstoIntros =
    4.18 -  NamedThmsFun(val name = "tendsto_intros"
    4.19 -               val description = "introduction rules for tendsto");
    4.20 +ML {*
    4.21 +structure Tendsto_Intros = Named_Thms
    4.22 +(
    4.23 +  val name = "tendsto_intros"
    4.24 +  val description = "introduction rules for tendsto"
    4.25 +)
    4.26  *}
    4.27  
    4.28 -setup TendstoIntros.setup
    4.29 +setup Tendsto_Intros.setup
    4.30  
    4.31  lemma topological_tendstoI:
    4.32    "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
     5.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Jul 02 17:33:36 2009 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Jul 02 17:34:14 2009 +0200
     5.3 @@ -373,7 +373,7 @@
     5.4             lthy''
     5.5             |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
     5.6                  map (Attrib.internal o K)
     5.7 -                    [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
     5.8 +                    [Simplifier.simp_add, Nitpick_Const_Simps.add]),
     5.9                  maps snd simps')
    5.10             |> snd
    5.11           end)
     6.1 --- a/src/HOL/OrderedGroup.thy	Thu Jul 02 17:33:36 2009 +0200
     6.2 +++ b/src/HOL/OrderedGroup.thy	Thu Jul 02 17:34:14 2009 +0200
     6.3 @@ -22,13 +22,15 @@
     6.4    \end{itemize}
     6.5  *}
     6.6  
     6.7 -ML{*
     6.8 -structure AlgebraSimps =
     6.9 -  NamedThmsFun(val name = "algebra_simps"
    6.10 -               val description = "algebra simplification rules");
    6.11 +ML {*
    6.12 +structure Algebra_Simps = Named_Thms
    6.13 +(
    6.14 +  val name = "algebra_simps"
    6.15 +  val description = "algebra simplification rules"
    6.16 +)
    6.17  *}
    6.18  
    6.19 -setup AlgebraSimps.setup
    6.20 +setup Algebra_Simps.setup
    6.21  
    6.22  text{* The rewrites accumulated in @{text algebra_simps} deal with the
    6.23  classical algebraic structures of groups, rings and family. They simplify
     7.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jul 02 17:33:36 2009 +0200
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jul 02 17:34:14 2009 +0200
     7.3 @@ -264,7 +264,7 @@
     7.4      thy2
     7.5      |> Sign.add_path (space_implode "_" new_type_names)
     7.6      |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
     7.7 -         [Nitpick_Const_Simp_Thms.add])]
     7.8 +         [Nitpick_Const_Simps.add])]
     7.9      ||> Sign.parent_path
    7.10      ||> Theory.checkpoint
    7.11      |-> (fn thms => pair (reccomb_names, Library.flat thms))
    7.12 @@ -337,7 +337,7 @@
    7.13            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    7.14    in
    7.15      thy2
    7.16 -    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
    7.17 +    |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
    7.18         o Context.Theory
    7.19      |> parent_path (#flat_names config)
    7.20      |> store_thmss "cases" new_type_names case_thms
     8.1 --- a/src/HOL/Tools/Function/fundef.ML	Thu Jul 02 17:33:36 2009 +0200
     8.2 +++ b/src/HOL/Tools/Function/fundef.ML	Thu Jul 02 17:34:14 2009 +0200
     8.3 @@ -37,12 +37,12 @@
     8.4  val simp_attribs = map (Attrib.internal o K)
     8.5      [Simplifier.simp_add,
     8.6       Code.add_default_eqn_attribute,
     8.7 -     Nitpick_Const_Simp_Thms.add,
     8.8 -     Quickcheck_RecFun_Simp_Thms.add]
     8.9 +     Nitpick_Const_Simps.add,
    8.10 +     Quickcheck_RecFun_Simps.add]
    8.11  
    8.12  val psimp_attribs = map (Attrib.internal o K)
    8.13      [Simplifier.simp_add,
    8.14 -     Nitpick_Const_Psimp_Thms.add]
    8.15 +     Nitpick_Const_Psimps.add]
    8.16  
    8.17  fun note_theorem ((name, atts), ths) =
    8.18    LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
    8.19 @@ -202,7 +202,7 @@
    8.20      "declaration of congruence rule for function definitions"
    8.21    #> setup_case_cong
    8.22    #> FundefRelation.setup
    8.23 -  #> FundefCommon.TerminationSimps.setup
    8.24 +  #> FundefCommon.Termination_Simps.setup
    8.25  
    8.26  val get_congs = FundefCtxTree.get_fundef_congs
    8.27  
     9.1 --- a/src/HOL/Tools/Function/fundef_common.ML	Thu Jul 02 17:33:36 2009 +0200
     9.2 +++ b/src/HOL/Tools/Function/fundef_common.ML	Thu Jul 02 17:34:14 2009 +0200
     9.3 @@ -144,7 +144,7 @@
     9.4  
     9.5  (* Simp rules for termination proofs *)
     9.6  
     9.7 -structure TerminationSimps = NamedThmsFun
     9.8 +structure Termination_Simps = Named_Thms
     9.9  (
    9.10    val name = "termination_simp" 
    9.11    val description = "Simplification rule for termination proofs"
    10.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 02 17:33:36 2009 +0200
    10.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 02 17:34:14 2009 +0200
    10.3 @@ -216,7 +216,8 @@
    10.4  
    10.5  fun lexicographic_order_tac ctxt =
    10.6    TRY (FundefCommon.apply_termination_rule ctxt 1)
    10.7 -  THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))
    10.8 +  THEN lex_order_tac ctxt
    10.9 +    (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
   10.10  
   10.11  val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
   10.12  
    11.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Thu Jul 02 17:33:36 2009 +0200
    11.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Thu Jul 02 17:34:14 2009 +0200
    11.3 @@ -1,7 +1,7 @@
    11.4  (*  Title:       HOL/Tools/Function/measure_functions.ML
    11.5      Author:      Alexander Krauss, TU Muenchen
    11.6  
    11.7 -Measure functions, generated heuristically
    11.8 +Measure functions, generated heuristically.
    11.9  *)
   11.10  
   11.11  signature MEASURE_FUNCTIONS =
   11.12 @@ -16,7 +16,8 @@
   11.13  struct 
   11.14  
   11.15  (** User-declared size functions **)
   11.16 -structure MeasureHeuristicRules = NamedThmsFun(
   11.17 +structure Measure_Heuristic_Rules = Named_Thms
   11.18 +(
   11.19    val name = "measure_function" 
   11.20    val description = "Rules that guide the heuristic generation of measure functions"
   11.21  );
   11.22 @@ -24,7 +25,7 @@
   11.23  fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
   11.24  
   11.25  fun find_measures ctxt T =
   11.26 -  DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1) 
   11.27 +  DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) 
   11.28      (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
   11.29        |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
   11.30    |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
   11.31 @@ -41,7 +42,7 @@
   11.32      @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
   11.33    | mk_funorder_funs T = [ constant_1 T ]
   11.34  
   11.35 -fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) =
   11.36 +fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
   11.37        map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
   11.38                    (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
   11.39    | mk_ext_base_funs ctxt T = find_measures ctxt T
   11.40 @@ -52,7 +53,7 @@
   11.41  
   11.42  val get_measure_functions = mk_all_measure_funs
   11.43  
   11.44 -val setup = MeasureHeuristicRules.setup
   11.45 +val setup = Measure_Heuristic_Rules.setup
   11.46  
   11.47  end
   11.48  
    12.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Jul 02 17:33:36 2009 +0200
    12.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Jul 02 17:34:14 2009 +0200
    12.3 @@ -405,7 +405,7 @@
    12.4  
    12.5  fun decomp_scnp orders ctxt =
    12.6    let
    12.7 -    val extra_simps = FundefCommon.TerminationSimps.get ctxt
    12.8 +    val extra_simps = FundefCommon.Termination_Simps.get ctxt
    12.9      val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
   12.10    in
   12.11      SIMPLE_METHOD
    13.1 --- a/src/HOL/Tools/Function/size.ML	Thu Jul 02 17:33:36 2009 +0200
    13.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Jul 02 17:34:14 2009 +0200
    13.3 @@ -209,7 +209,7 @@
    13.4  
    13.5      val ([size_thms], thy'') =  PureThy.add_thmss
    13.6        [((Binding.name "size", size_eqns),
    13.7 -        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
    13.8 +        [Simplifier.simp_add, Nitpick_Const_Simps.add,
    13.9           Thm.declaration_attribute
   13.10               (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
   13.11  
    14.1 --- a/src/HOL/Tools/arith_data.ML	Thu Jul 02 17:33:36 2009 +0200
    14.2 +++ b/src/HOL/Tools/arith_data.ML	Thu Jul 02 17:34:14 2009 +0200
    14.3 @@ -28,7 +28,8 @@
    14.4  
    14.5  (* slots for plugging in arithmetic facts and tactics *)
    14.6  
    14.7 -structure Arith_Facts = NamedThmsFun(
    14.8 +structure Arith_Facts = Named_Thms
    14.9 +(
   14.10    val name = "arith"
   14.11    val description = "arith facts - only ground formulas"
   14.12  );
    15.1 --- a/src/HOL/Tools/inductive.ML	Thu Jul 02 17:33:36 2009 +0200
    15.2 +++ b/src/HOL/Tools/inductive.ML	Thu Jul 02 17:34:14 2009 +0200
    15.3 @@ -694,7 +694,7 @@
    15.4        LocalTheory.notes kind
    15.5          (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
    15.6             [Attrib.internal (K (ContextRules.intro_query NONE)),
    15.7 -            Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>>
    15.8 +            Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
    15.9        map (hd o snd);
   15.10      val (((_, elims'), (_, [induct'])), ctxt2) =
   15.11        ctxt1 |>
    16.1 --- a/src/HOL/Tools/old_primrec.ML	Thu Jul 02 17:33:36 2009 +0200
    16.2 +++ b/src/HOL/Tools/old_primrec.ML	Thu Jul 02 17:34:14 2009 +0200
    16.3 @@ -283,8 +283,8 @@
    16.4      val simps'' = maps snd simps';
    16.5    in
    16.6      thy''
    16.7 -    |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
    16.8 -                        Code.add_default_eqn_attribute]), simps'')
    16.9 +    |> note (("simps",
   16.10 +        [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'')
   16.11      |> snd
   16.12      |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
   16.13      |> snd
    17.1 --- a/src/HOL/Tools/primrec.ML	Thu Jul 02 17:33:36 2009 +0200
    17.2 +++ b/src/HOL/Tools/primrec.ML	Thu Jul 02 17:34:14 2009 +0200
    17.3 @@ -272,7 +272,7 @@
    17.4        (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
    17.5      fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
    17.6        map (Attrib.internal o K)
    17.7 -        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]);
    17.8 +        [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]);
    17.9    in
   17.10      lthy
   17.11      |> set_group ? LocalTheory.set_group (serial_string ())
    18.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 02 17:33:36 2009 +0200
    18.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 02 17:34:14 2009 +0200
    18.3 @@ -244,7 +244,7 @@
    18.4      |-> (fn proto_simps => prove_simps proto_simps)
    18.5      |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
    18.6             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    18.7 -          [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]),
    18.8 +          [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]),
    18.9              simps))
   18.10      |> snd
   18.11    end
    19.1 --- a/src/HOL/Tools/recdef.ML	Thu Jul 02 17:33:36 2009 +0200
    19.2 +++ b/src/HOL/Tools/recdef.ML	Thu Jul 02 17:34:14 2009 +0200
    19.3 @@ -207,8 +207,8 @@
    19.4          tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
    19.5                 congs wfs name R eqs;
    19.6      val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
    19.7 -    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
    19.8 -      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else [];
    19.9 +    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simps.add,
   19.10 +      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
   19.11  
   19.12      val ((simps' :: rules', [induct']), thy) =
   19.13        thy
    20.1 --- a/src/HOL/Tools/record.ML	Thu Jul 02 17:33:36 2009 +0200
    20.2 +++ b/src/HOL/Tools/record.ML	Thu Jul 02 17:34:14 2009 +0200
    20.3 @@ -2192,7 +2192,7 @@
    20.4        thms_thy
    20.5        |> (snd oo PureThy.add_thmss)
    20.6            [((Binding.name "simps", sel_upd_simps),
    20.7 -            [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
    20.8 +            [Simplifier.simp_add, Nitpick_Const_Simps.add]),
    20.9             ((Binding.name "iffs", iffs), [iff_add])]
   20.10        |> put_record name (make_record_info args parent fields extension induct_scheme')
   20.11        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
    21.1 --- a/src/HOL/ex/Numeral.thy	Thu Jul 02 17:33:36 2009 +0200
    21.2 +++ b/src/HOL/ex/Numeral.thy	Thu Jul 02 17:34:14 2009 +0200
    21.3 @@ -93,11 +93,14 @@
    21.4  subsection {* Numeral operations *}
    21.5  
    21.6  ML {*
    21.7 -structure DigSimps =
    21.8 -  NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
    21.9 +structure Dig_Simps = Named_Thms
   21.10 +(
   21.11 +  val name = "numeral"
   21.12 +  val description = "Simplification rules for numerals"
   21.13 +)
   21.14  *}
   21.15  
   21.16 -setup DigSimps.setup
   21.17 +setup Dig_Simps.setup
   21.18  
   21.19  instantiation num :: "{plus,times,ord}"
   21.20  begin
    22.1 --- a/src/HOLCF/Cont.thy	Thu Jul 02 17:33:36 2009 +0200
    22.2 +++ b/src/HOLCF/Cont.thy	Thu Jul 02 17:34:14 2009 +0200
    22.3 @@ -140,8 +140,11 @@
    22.4  subsection {* Continuity simproc *}
    22.5  
    22.6  ML {*
    22.7 -structure Cont2ContData = NamedThmsFun
    22.8 -  ( val name = "cont2cont" val description = "continuity intro rule" )
    22.9 +structure Cont2ContData = Named_Thms
   22.10 +(
   22.11 +  val name = "cont2cont"
   22.12 +  val description = "continuity intro rule"
   22.13 +)
   22.14  *}
   22.15  
   22.16  setup Cont2ContData.setup
    23.1 --- a/src/Tools/atomize_elim.ML	Thu Jul 02 17:33:36 2009 +0200
    23.2 +++ b/src/Tools/atomize_elim.ML	Thu Jul 02 17:34:14 2009 +0200
    23.3 @@ -20,7 +20,9 @@
    23.4  struct
    23.5  
    23.6  (* theory data *)
    23.7 -structure AtomizeElimData = NamedThmsFun(
    23.8 +
    23.9 +structure AtomizeElimData = Named_Thms
   23.10 +(
   23.11    val name = "atomize_elim";
   23.12    val description = "atomize_elim rewrite rule";
   23.13  );
    24.1 --- a/src/ZF/UNITY/Constrains.thy	Thu Jul 02 17:33:36 2009 +0200
    24.2 +++ b/src/ZF/UNITY/Constrains.thy	Thu Jul 02 17:34:14 2009 +0200
    24.3 @@ -462,7 +462,11 @@
    24.4  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
    24.5  
    24.6  (*To allow expansion of the program's definition when appropriate*)
    24.7 -structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions");
    24.8 +structure Program_Defs = Named_Thms
    24.9 +(
   24.10 +  val name = "program"
   24.11 +  val description = "program definitions"
   24.12 +);
   24.13  
   24.14  (*proves "co" properties when the program is specified*)
   24.15  
   24.16 @@ -478,7 +482,7 @@
   24.17                (* Three subgoals *)
   24.18                rewrite_goal_tac [@{thm st_set_def}] 3,
   24.19                REPEAT (force_tac css 2),
   24.20 -              full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1,
   24.21 +              full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
   24.22                ALLGOALS (clarify_tac cs),
   24.23                REPEAT (FIRSTGOAL (etac disjE)),
   24.24                ALLGOALS (clarify_tac cs),
   24.25 @@ -493,7 +497,7 @@
   24.26      rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
   24.27  *}
   24.28  
   24.29 -setup ProgramDefs.setup
   24.30 +setup Program_Defs.setup
   24.31  
   24.32  method_setup safety = {*
   24.33    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
    25.1 --- a/src/ZF/UNITY/SubstAx.thy	Thu Jul 02 17:33:36 2009 +0200
    25.2 +++ b/src/ZF/UNITY/SubstAx.thy	Thu Jul 02 17:34:14 2009 +0200
    25.3 @@ -359,7 +359,7 @@
    25.4                    REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    25.5                                      @{thm EnsuresI}, @{thm ensuresI}] 1),
    25.6                (*now there are two subgoals: co & transient*)
    25.7 -              simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
    25.8 +              simp_tac (ss addsimps (Program_Defs.get ctxt)) 2,
    25.9                res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
   25.10                   (*simplify the command's domain*)
   25.11                simp_tac (ss addsimps [@{thm domain_def}]) 3,