merged
authorwenzelm
Thu Jul 02 22:18:02 2009 +0200 (2009-07-02)
changeset 31917342a0bad5adf
parent 31916 f3227bb306a4
parent 31905 4263be178c8f
child 31918 60d573a5d061
merged
     1.1 --- a/NEWS	Thu Jul 02 21:24:32 2009 +0200
     1.2 +++ b/NEWS	Thu Jul 02 22:18:02 2009 +0200
     1.3 @@ -37,11 +37,13 @@
     1.4  * New method "linarith" invokes existing linear arithmetic decision
     1.5  procedure only.
     1.6  
     1.7 -* Implementation of quickcheck using generic code generator; default generators
     1.8 -are provided for all suitable HOL types, records and datatypes.
     1.9 -
    1.10 -* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
    1.11 -Set.Pow_def and Set.image_def.  INCOMPATIBILITY.
    1.12 +* Implementation of quickcheck using generic code generator; default
    1.13 +generators are provided for all suitable HOL types, records and
    1.14 +datatypes.
    1.15 +
    1.16 +* Constants Set.Pow and Set.image now with authentic syntax;
    1.17 +object-logic definitions Set.Pow_def and Set.image_def.
    1.18 +INCOMPATIBILITY.
    1.19  
    1.20  * Renamed theorems:
    1.21  Suc_eq_add_numeral_1 -> Suc_eq_plus1
    1.22 @@ -49,10 +51,12 @@
    1.23  Suc_plus1 -> Suc_eq_plus1
    1.24  
    1.25  * New sledgehammer option "Full Types" in Proof General settings menu.
    1.26 -Causes full type information to be output to the ATPs. This slows ATPs down
    1.27 -considerably but eliminates a source of unsound "proofs" that fail later.
    1.28 -
    1.29 -* Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.:
    1.30 +Causes full type information to be output to the ATPs.  This slows
    1.31 +ATPs down considerably but eliminates a source of unsound "proofs"
    1.32 +that fail later.
    1.33 +
    1.34 +* Discontinued ancient tradition to suffix certain ML module names
    1.35 +with "_package", e.g.:
    1.36  
    1.37      DatatypePackage ~> Datatype
    1.38      InductivePackage ~> Inductive
    1.39 @@ -61,31 +65,35 @@
    1.40  
    1.41  INCOMPATIBILITY.
    1.42  
    1.43 -* NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory.
    1.44 -If possible, use NewNumberTheory, not NumberTheory.
    1.45 +* NewNumberTheory: Jeremy Avigad's new version of part of
    1.46 +NumberTheory.  If possible, use NewNumberTheory, not NumberTheory.
    1.47  
    1.48  * Simplified interfaces of datatype module.  INCOMPATIBILITY.
    1.49  
    1.50 -* Abbreviation "arbitrary" of "undefined" has disappeared; use "undefined" directly.
    1.51 -INCOMPATIBILITY.
    1.52 -
    1.53 -* New evaluator "approximate" approximates an real valued term using the same method as the
    1.54 -approximation method. 
    1.55 -
    1.56 -* "approximate" supports now arithmetic expressions as boundaries of intervals and implements
    1.57 -interval splitting and taylor series expansion.
    1.58 -
    1.59 -* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in DERIV_intros
    1.60 -assumes composition with an additional function and matches a variable to the
    1.61 -derivative, which has to be solved by the simplifier. Hence
    1.62 -(auto intro!: DERIV_intros) computes the derivative of most elementary terms.
    1.63 -
    1.64 -* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by:
    1.65 -(auto intro!: DERIV_intros)
    1.66 -INCOMPATIBILITY.
    1.67 +* Abbreviation "arbitrary" of "undefined" has disappeared; use
    1.68 +"undefined" directly.  INCOMPATIBILITY.
    1.69 +
    1.70 +* New evaluator "approximate" approximates an real valued term using
    1.71 +the same method as the approximation method.
    1.72 +
    1.73 +* Method "approximate" supports now arithmetic expressions as
    1.74 +boundaries of intervals and implements interval splitting and Taylor
    1.75 +series expansion.
    1.76 +
    1.77 +* Changed DERIV_intros to a dynamic fact (via Named_Thms).  Each of
    1.78 +the theorems in DERIV_intros assumes composition with an additional
    1.79 +function and matches a variable to the derivative, which has to be
    1.80 +solved by the simplifier.  Hence (auto intro!: DERIV_intros) computes
    1.81 +the derivative of most elementary terms.
    1.82 +
    1.83 +* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
    1.84 +replaced by: (auto intro!: DERIV_intros).  INCOMPATIBILITY.
    1.85 +
    1.86  
    1.87  *** ML ***
    1.88  
    1.89 +* Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
    1.90 +
    1.91  * Eliminated old Attrib.add_attributes, Method.add_methods and related
    1.92  cominators for "args".  INCOMPATIBILITY, need to use simplified
    1.93  Attrib/Method.setup introduced in Isabelle2009.
     2.1 --- a/src/CCL/Wfd.thy	Thu Jul 02 21:24:32 2009 +0200
     2.2 +++ b/src/CCL/Wfd.thy	Thu Jul 02 22:18:02 2009 +0200
     2.3 @@ -495,7 +495,7 @@
     2.4  ML {*
     2.5  
     2.6  local
     2.7 -  structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules");
     2.8 +  structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
     2.9  in
    2.10  
    2.11  fun eval_tac ctxt ths =
     3.1 --- a/src/HOL/Deriv.thy	Thu Jul 02 21:24:32 2009 +0200
     3.2 +++ b/src/HOL/Deriv.thy	Thu Jul 02 22:18:02 2009 +0200
     3.3 @@ -315,14 +315,14 @@
     3.4  
     3.5  text {* @{text "DERIV_intros"} *}
     3.6  ML {*
     3.7 -structure DerivIntros = NamedThmsFun
     3.8 +structure Deriv_Intros = Named_Thms
     3.9  (
    3.10    val name = "DERIV_intros"
    3.11    val description = "DERIV introduction rules"
    3.12  )
    3.13  *}
    3.14  
    3.15 -setup DerivIntros.setup
    3.16 +setup Deriv_Intros.setup
    3.17  
    3.18  lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
    3.19    by simp
     4.1 --- a/src/HOL/HOL.thy	Thu Jul 02 21:24:32 2009 +0200
     4.2 +++ b/src/HOL/HOL.thy	Thu Jul 02 22:18:02 2009 +0200
     4.3 @@ -923,9 +923,11 @@
     4.4  ML_Antiquote.value "claset"
     4.5    (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())");
     4.6  
     4.7 -structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
     4.8 +structure ResAtpset = Named_Thms
     4.9 +  (val name = "atp" val description = "ATP rules");
    4.10  
    4.11 -structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP");
    4.12 +structure ResBlacklist = Named_Thms
    4.13 +  (val name = "noatp" val description = "theorems blacklisted for ATP");
    4.14  *}
    4.15  
    4.16  text {*ResBlacklist holds theorems blacklisted to sledgehammer. 
    4.17 @@ -1982,19 +1984,18 @@
    4.18    Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
    4.19  *} "solve goal by normalization"
    4.20  
    4.21 +
    4.22  subsubsection {* Quickcheck *}
    4.23  
    4.24  ML {*
    4.25 -structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun
    4.26 +structure Quickcheck_RecFun_Simps = Named_Thms
    4.27  (
    4.28    val name = "quickcheck_recfun_simp"
    4.29    val description = "simplification rules of recursive functions as needed by Quickcheck"
    4.30  )
    4.31  *}
    4.32  
    4.33 -setup {*
    4.34 -  Quickcheck_RecFun_Simp_Thms.setup
    4.35 -*}
    4.36 +setup Quickcheck_RecFun_Simps.setup
    4.37  
    4.38  setup {*
    4.39    Quickcheck.add_generator ("SML", Codegen.test_term)
    4.40 @@ -2008,22 +2009,22 @@
    4.41  text {* This will be relocated once Nitpick is moved to HOL. *}
    4.42  
    4.43  ML {*
    4.44 -structure Nitpick_Const_Def_Thms = NamedThmsFun
    4.45 +structure Nitpick_Const_Defs = Named_Thms
    4.46  (
    4.47    val name = "nitpick_const_def"
    4.48    val description = "alternative definitions of constants as needed by Nitpick"
    4.49  )
    4.50 -structure Nitpick_Const_Simp_Thms = NamedThmsFun
    4.51 +structure Nitpick_Const_Simps = Named_Thms
    4.52  (
    4.53    val name = "nitpick_const_simp"
    4.54    val description = "equational specification of constants as needed by Nitpick"
    4.55  )
    4.56 -structure Nitpick_Const_Psimp_Thms = NamedThmsFun
    4.57 +structure Nitpick_Const_Psimps = Named_Thms
    4.58  (
    4.59    val name = "nitpick_const_psimp"
    4.60    val description = "partial equational specification of constants as needed by Nitpick"
    4.61  )
    4.62 -structure Nitpick_Ind_Intro_Thms = NamedThmsFun
    4.63 +structure Nitpick_Ind_Intros = Named_Thms
    4.64  (
    4.65    val name = "nitpick_ind_intro"
    4.66    val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    4.67 @@ -2031,10 +2032,10 @@
    4.68  *}
    4.69  
    4.70  setup {*
    4.71 -  Nitpick_Const_Def_Thms.setup
    4.72 -  #> Nitpick_Const_Simp_Thms.setup
    4.73 -  #> Nitpick_Const_Psimp_Thms.setup
    4.74 -  #> Nitpick_Ind_Intro_Thms.setup
    4.75 +  Nitpick_Const_Defs.setup
    4.76 +  #> Nitpick_Const_Simps.setup
    4.77 +  #> Nitpick_Const_Psimps.setup
    4.78 +  #> Nitpick_Ind_Intros.setup
    4.79  *}
    4.80  
    4.81  
     5.1 --- a/src/HOL/Limits.thy	Thu Jul 02 21:24:32 2009 +0200
     5.2 +++ b/src/HOL/Limits.thy	Thu Jul 02 22:18:02 2009 +0200
     5.3 @@ -350,7 +350,7 @@
     5.4  lemmas Zfun_mult_left = mult.Zfun_left
     5.5  
     5.6  
     5.7 -subsection{* Limits *}
     5.8 +subsection {* Limits *}
     5.9  
    5.10  definition
    5.11    tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
    5.12 @@ -358,13 +358,15 @@
    5.13  where [code del]:
    5.14    "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
    5.15  
    5.16 -ML{*
    5.17 -structure TendstoIntros =
    5.18 -  NamedThmsFun(val name = "tendsto_intros"
    5.19 -               val description = "introduction rules for tendsto");
    5.20 +ML {*
    5.21 +structure Tendsto_Intros = Named_Thms
    5.22 +(
    5.23 +  val name = "tendsto_intros"
    5.24 +  val description = "introduction rules for tendsto"
    5.25 +)
    5.26  *}
    5.27  
    5.28 -setup TendstoIntros.setup
    5.29 +setup Tendsto_Intros.setup
    5.30  
    5.31  lemma topological_tendstoI:
    5.32    "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
     6.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Jul 02 21:24:32 2009 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Jul 02 22:18:02 2009 +0200
     6.3 @@ -373,7 +373,7 @@
     6.4             lthy''
     6.5             |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
     6.6                  map (Attrib.internal o K)
     6.7 -                    [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
     6.8 +                    [Simplifier.simp_add, Nitpick_Const_Simps.add]),
     6.9                  maps snd simps')
    6.10             |> snd
    6.11           end)
     7.1 --- a/src/HOL/OrderedGroup.thy	Thu Jul 02 21:24:32 2009 +0200
     7.2 +++ b/src/HOL/OrderedGroup.thy	Thu Jul 02 22:18:02 2009 +0200
     7.3 @@ -22,13 +22,15 @@
     7.4    \end{itemize}
     7.5  *}
     7.6  
     7.7 -ML{*
     7.8 -structure AlgebraSimps =
     7.9 -  NamedThmsFun(val name = "algebra_simps"
    7.10 -               val description = "algebra simplification rules");
    7.11 +ML {*
    7.12 +structure Algebra_Simps = Named_Thms
    7.13 +(
    7.14 +  val name = "algebra_simps"
    7.15 +  val description = "algebra simplification rules"
    7.16 +)
    7.17  *}
    7.18  
    7.19 -setup AlgebraSimps.setup
    7.20 +setup Algebra_Simps.setup
    7.21  
    7.22  text{* The rewrites accumulated in @{text algebra_simps} deal with the
    7.23  classical algebraic structures of groups, rings and family. They simplify
     8.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jul 02 21:24:32 2009 +0200
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jul 02 22:18:02 2009 +0200
     8.3 @@ -264,7 +264,7 @@
     8.4      thy2
     8.5      |> Sign.add_path (space_implode "_" new_type_names)
     8.6      |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
     8.7 -         [Nitpick_Const_Simp_Thms.add])]
     8.8 +         [Nitpick_Const_Simps.add])]
     8.9      ||> Sign.parent_path
    8.10      ||> Theory.checkpoint
    8.11      |-> (fn thms => pair (reccomb_names, Library.flat thms))
    8.12 @@ -337,7 +337,7 @@
    8.13            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    8.14    in
    8.15      thy2
    8.16 -    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
    8.17 +    |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
    8.18         o Context.Theory
    8.19      |> parent_path (#flat_names config)
    8.20      |> store_thmss "cases" new_type_names case_thms
     9.1 --- a/src/HOL/Tools/Function/fundef.ML	Thu Jul 02 21:24:32 2009 +0200
     9.2 +++ b/src/HOL/Tools/Function/fundef.ML	Thu Jul 02 22:18:02 2009 +0200
     9.3 @@ -37,12 +37,12 @@
     9.4  val simp_attribs = map (Attrib.internal o K)
     9.5      [Simplifier.simp_add,
     9.6       Code.add_default_eqn_attribute,
     9.7 -     Nitpick_Const_Simp_Thms.add,
     9.8 -     Quickcheck_RecFun_Simp_Thms.add]
     9.9 +     Nitpick_Const_Simps.add,
    9.10 +     Quickcheck_RecFun_Simps.add]
    9.11  
    9.12  val psimp_attribs = map (Attrib.internal o K)
    9.13      [Simplifier.simp_add,
    9.14 -     Nitpick_Const_Psimp_Thms.add]
    9.15 +     Nitpick_Const_Psimps.add]
    9.16  
    9.17  fun note_theorem ((name, atts), ths) =
    9.18    LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
    9.19 @@ -202,7 +202,7 @@
    9.20      "declaration of congruence rule for function definitions"
    9.21    #> setup_case_cong
    9.22    #> FundefRelation.setup
    9.23 -  #> FundefCommon.TerminationSimps.setup
    9.24 +  #> FundefCommon.Termination_Simps.setup
    9.25  
    9.26  val get_congs = FundefCtxTree.get_fundef_congs
    9.27  
    10.1 --- a/src/HOL/Tools/Function/fundef_common.ML	Thu Jul 02 21:24:32 2009 +0200
    10.2 +++ b/src/HOL/Tools/Function/fundef_common.ML	Thu Jul 02 22:18:02 2009 +0200
    10.3 @@ -144,7 +144,7 @@
    10.4  
    10.5  (* Simp rules for termination proofs *)
    10.6  
    10.7 -structure TerminationSimps = NamedThmsFun
    10.8 +structure Termination_Simps = Named_Thms
    10.9  (
   10.10    val name = "termination_simp" 
   10.11    val description = "Simplification rule for termination proofs"
    11.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 02 21:24:32 2009 +0200
    11.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 02 22:18:02 2009 +0200
    11.3 @@ -216,7 +216,8 @@
    11.4  
    11.5  fun lexicographic_order_tac ctxt =
    11.6    TRY (FundefCommon.apply_termination_rule ctxt 1)
    11.7 -  THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))
    11.8 +  THEN lex_order_tac ctxt
    11.9 +    (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
   11.10  
   11.11  val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
   11.12  
    12.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Thu Jul 02 21:24:32 2009 +0200
    12.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Thu Jul 02 22:18:02 2009 +0200
    12.3 @@ -1,7 +1,7 @@
    12.4  (*  Title:       HOL/Tools/Function/measure_functions.ML
    12.5      Author:      Alexander Krauss, TU Muenchen
    12.6  
    12.7 -Measure functions, generated heuristically
    12.8 +Measure functions, generated heuristically.
    12.9  *)
   12.10  
   12.11  signature MEASURE_FUNCTIONS =
   12.12 @@ -16,7 +16,8 @@
   12.13  struct 
   12.14  
   12.15  (** User-declared size functions **)
   12.16 -structure MeasureHeuristicRules = NamedThmsFun(
   12.17 +structure Measure_Heuristic_Rules = Named_Thms
   12.18 +(
   12.19    val name = "measure_function" 
   12.20    val description = "Rules that guide the heuristic generation of measure functions"
   12.21  );
   12.22 @@ -24,7 +25,7 @@
   12.23  fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
   12.24  
   12.25  fun find_measures ctxt T =
   12.26 -  DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1) 
   12.27 +  DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) 
   12.28      (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
   12.29        |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
   12.30    |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
   12.31 @@ -41,7 +42,7 @@
   12.32      @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
   12.33    | mk_funorder_funs T = [ constant_1 T ]
   12.34  
   12.35 -fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) =
   12.36 +fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
   12.37        map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
   12.38                    (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
   12.39    | mk_ext_base_funs ctxt T = find_measures ctxt T
   12.40 @@ -52,7 +53,7 @@
   12.41  
   12.42  val get_measure_functions = mk_all_measure_funs
   12.43  
   12.44 -val setup = MeasureHeuristicRules.setup
   12.45 +val setup = Measure_Heuristic_Rules.setup
   12.46  
   12.47  end
   12.48  
    13.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Jul 02 21:24:32 2009 +0200
    13.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Jul 02 22:18:02 2009 +0200
    13.3 @@ -405,7 +405,7 @@
    13.4  
    13.5  fun decomp_scnp orders ctxt =
    13.6    let
    13.7 -    val extra_simps = FundefCommon.TerminationSimps.get ctxt
    13.8 +    val extra_simps = FundefCommon.Termination_Simps.get ctxt
    13.9      val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
   13.10    in
   13.11      SIMPLE_METHOD
    14.1 --- a/src/HOL/Tools/Function/size.ML	Thu Jul 02 21:24:32 2009 +0200
    14.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Jul 02 22:18:02 2009 +0200
    14.3 @@ -209,7 +209,7 @@
    14.4  
    14.5      val ([size_thms], thy'') =  PureThy.add_thmss
    14.6        [((Binding.name "size", size_eqns),
    14.7 -        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
    14.8 +        [Simplifier.simp_add, Nitpick_Const_Simps.add,
    14.9           Thm.declaration_attribute
   14.10               (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
   14.11  
    15.1 --- a/src/HOL/Tools/arith_data.ML	Thu Jul 02 21:24:32 2009 +0200
    15.2 +++ b/src/HOL/Tools/arith_data.ML	Thu Jul 02 22:18:02 2009 +0200
    15.3 @@ -28,7 +28,8 @@
    15.4  
    15.5  (* slots for plugging in arithmetic facts and tactics *)
    15.6  
    15.7 -structure Arith_Facts = NamedThmsFun(
    15.8 +structure Arith_Facts = Named_Thms
    15.9 +(
   15.10    val name = "arith"
   15.11    val description = "arith facts - only ground formulas"
   15.12  );
    16.1 --- a/src/HOL/Tools/inductive.ML	Thu Jul 02 21:24:32 2009 +0200
    16.2 +++ b/src/HOL/Tools/inductive.ML	Thu Jul 02 22:18:02 2009 +0200
    16.3 @@ -694,7 +694,7 @@
    16.4        LocalTheory.notes kind
    16.5          (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
    16.6             [Attrib.internal (K (ContextRules.intro_query NONE)),
    16.7 -            Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>>
    16.8 +            Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
    16.9        map (hd o snd);
   16.10      val (((_, elims'), (_, [induct'])), ctxt2) =
   16.11        ctxt1 |>
    17.1 --- a/src/HOL/Tools/old_primrec.ML	Thu Jul 02 21:24:32 2009 +0200
    17.2 +++ b/src/HOL/Tools/old_primrec.ML	Thu Jul 02 22:18:02 2009 +0200
    17.3 @@ -283,8 +283,8 @@
    17.4      val simps'' = maps snd simps';
    17.5    in
    17.6      thy''
    17.7 -    |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
    17.8 -                        Code.add_default_eqn_attribute]), simps'')
    17.9 +    |> note (("simps",
   17.10 +        [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'')
   17.11      |> snd
   17.12      |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
   17.13      |> snd
    18.1 --- a/src/HOL/Tools/primrec.ML	Thu Jul 02 21:24:32 2009 +0200
    18.2 +++ b/src/HOL/Tools/primrec.ML	Thu Jul 02 22:18:02 2009 +0200
    18.3 @@ -272,7 +272,7 @@
    18.4        (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
    18.5      fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
    18.6        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    in
   18.10      lthy
   18.11      |> set_group ? LocalTheory.set_group (serial_string ())
    19.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 02 21:24:32 2009 +0200
    19.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Jul 02 22:18:02 2009 +0200
    19.3 @@ -244,7 +244,7 @@
    19.4      |-> (fn proto_simps => prove_simps proto_simps)
    19.5      |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
    19.6             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    19.7 -          [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]),
    19.8 +          [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]),
    19.9              simps))
   19.10      |> snd
   19.11    end
    20.1 --- a/src/HOL/Tools/recdef.ML	Thu Jul 02 21:24:32 2009 +0200
    20.2 +++ b/src/HOL/Tools/recdef.ML	Thu Jul 02 22:18:02 2009 +0200
    20.3 @@ -207,8 +207,8 @@
    20.4          tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
    20.5                 congs wfs name R eqs;
    20.6      val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
    20.7 -    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
    20.8 -      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else [];
    20.9 +    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simps.add,
   20.10 +      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
   20.11  
   20.12      val ((simps' :: rules', [induct']), thy) =
   20.13        thy
    21.1 --- a/src/HOL/Tools/record.ML	Thu Jul 02 21:24:32 2009 +0200
    21.2 +++ b/src/HOL/Tools/record.ML	Thu Jul 02 22:18:02 2009 +0200
    21.3 @@ -2192,7 +2192,7 @@
    21.4        thms_thy
    21.5        |> (snd oo PureThy.add_thmss)
    21.6            [((Binding.name "simps", sel_upd_simps),
    21.7 -            [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
    21.8 +            [Simplifier.simp_add, Nitpick_Const_Simps.add]),
    21.9             ((Binding.name "iffs", iffs), [iff_add])]
   21.10        |> put_record name (make_record_info args parent fields extension induct_scheme')
   21.11        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
    22.1 --- a/src/HOL/ex/Numeral.thy	Thu Jul 02 21:24:32 2009 +0200
    22.2 +++ b/src/HOL/ex/Numeral.thy	Thu Jul 02 22:18:02 2009 +0200
    22.3 @@ -93,11 +93,14 @@
    22.4  subsection {* Numeral operations *}
    22.5  
    22.6  ML {*
    22.7 -structure DigSimps =
    22.8 -  NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
    22.9 +structure Dig_Simps = Named_Thms
   22.10 +(
   22.11 +  val name = "numeral"
   22.12 +  val description = "Simplification rules for numerals"
   22.13 +)
   22.14  *}
   22.15  
   22.16 -setup DigSimps.setup
   22.17 +setup Dig_Simps.setup
   22.18  
   22.19  instantiation num :: "{plus,times,ord}"
   22.20  begin
    23.1 --- a/src/HOLCF/Cont.thy	Thu Jul 02 21:24:32 2009 +0200
    23.2 +++ b/src/HOLCF/Cont.thy	Thu Jul 02 22:18:02 2009 +0200
    23.3 @@ -140,8 +140,11 @@
    23.4  subsection {* Continuity simproc *}
    23.5  
    23.6  ML {*
    23.7 -structure Cont2ContData = NamedThmsFun
    23.8 -  ( val name = "cont2cont" val description = "continuity intro rule" )
    23.9 +structure Cont2ContData = Named_Thms
   23.10 +(
   23.11 +  val name = "cont2cont"
   23.12 +  val description = "continuity intro rule"
   23.13 +)
   23.14  *}
   23.15  
   23.16  setup Cont2ContData.setup
    24.1 --- a/src/Pure/Isar/class.ML	Thu Jul 02 21:24:32 2009 +0200
    24.2 +++ b/src/Pure/Isar/class.ML	Thu Jul 02 22:18:02 2009 +0200
    24.3 @@ -90,7 +90,7 @@
    24.4      val sup_of_classes = map (snd o rules thy) sups;
    24.5      val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
    24.6      val axclass_intro = #intro (AxClass.get_info thy class);
    24.7 -    val base_sort_trivs = Drule.sort_triv thy (aT, base_sort);
    24.8 +    val base_sort_trivs = Thm.sort_triv thy (aT, base_sort);
    24.9      val tac = REPEAT (SOMEGOAL
   24.10        (Tactic.match_tac (axclass_intro :: sup_of_classes
   24.11           @ loc_axiom_intros @ base_sort_trivs)
    25.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Jul 02 21:24:32 2009 +0200
    25.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu Jul 02 22:18:02 2009 +0200
    25.3 @@ -54,6 +54,7 @@
    25.4         (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
    25.5         (Binding.name "Hyp", propT --> proofT, NoSyn),
    25.6         (Binding.name "Oracle", propT --> proofT, NoSyn),
    25.7 +       (Binding.name "Inclass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
    25.8         (Binding.name "MinProof", proofT, Delimfix "?")]
    25.9    |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
   25.10    |> Sign.add_syntax_i
   25.11 @@ -112,6 +113,12 @@
   25.12                     | NONE => error ("Unknown theorem " ^ quote name))
   25.13                   end
   25.14               | _ => error ("Illegal proof constant name: " ^ quote s))
   25.15 +      | prf_of Ts (Const ("Inclass", _) $ Const (c_class, _)) =
   25.16 +          (case try Logic.class_of_const c_class of
   25.17 +            SOME c =>
   25.18 +              change_type (if ty then SOME Ts else NONE)
   25.19 +                (Inclass (TVar ((Name.aT, 0), []), c))
   25.20 +          | NONE => error ("Bad class constant: " ^ quote c_class))
   25.21        | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
   25.22        | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
   25.23        | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
   25.24 @@ -141,6 +148,7 @@
   25.25  val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
   25.26  val Hypt = Const ("Hyp", propT --> proofT);
   25.27  val Oraclet = Const ("Oracle", propT --> proofT);
   25.28 +val Inclasst = Const ("Inclass", (Term.itselfT dummyT --> propT) --> proofT);
   25.29  val MinProoft = Const ("MinProof", proofT);
   25.30  
   25.31  val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
   25.32 @@ -153,6 +161,8 @@
   25.33    | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
   25.34    | term_of _ (PAxm (name, _, SOME Ts)) =
   25.35        mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
   25.36 +  | term_of _ (Inclass (T, c)) =
   25.37 +      mk_tyapp [T] (Inclasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
   25.38    | term_of _ (PBound i) = Bound i
   25.39    | term_of Ts (Abst (s, opT, prf)) =
   25.40        let val T = the_default dummyT opT
    26.1 --- a/src/Pure/Proof/reconstruct.ML	Thu Jul 02 21:24:32 2009 +0200
    26.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 02 22:18:02 2009 +0200
    26.3 @@ -140,7 +140,8 @@
    26.4            let
    26.5              val tvars = OldTerm.term_tvars prop;
    26.6              val tfrees = OldTerm.term_tfrees prop;
    26.7 -            val (env', Ts) = (case opTs of
    26.8 +            val (env', Ts) =
    26.9 +              (case opTs of
   26.10                  NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
   26.11                | SOME Ts => (env, Ts));
   26.12              val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
   26.13 @@ -222,6 +223,8 @@
   26.14            mk_cnstrts_atom env vTs prop opTs prf
   26.15        | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
   26.16            mk_cnstrts_atom env vTs prop opTs prf
   26.17 +      | mk_cnstrts env _ _ vTs (prf as Inclass (T, c)) =
   26.18 +          mk_cnstrts_atom env vTs (Logic.mk_inclass (T, c)) NONE prf
   26.19        | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
   26.20            mk_cnstrts_atom env vTs prop opTs prf
   26.21        | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
   26.22 @@ -318,6 +321,7 @@
   26.23    | prop_of0 Hs (Hyp t) = t
   26.24    | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
   26.25    | prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
   26.26 +  | prop_of0 Hs (Inclass (T, c)) = Logic.mk_inclass (T, c)
   26.27    | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
   26.28    | prop_of0 _ _ = error "prop_of: partial proof object";
   26.29  
    27.1 --- a/src/Pure/Tools/named_thms.ML	Thu Jul 02 21:24:32 2009 +0200
    27.2 +++ b/src/Pure/Tools/named_thms.ML	Thu Jul 02 22:18:02 2009 +0200
    27.3 @@ -14,7 +14,7 @@
    27.4    val setup: theory -> theory
    27.5  end;
    27.6  
    27.7 -functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
    27.8 +functor Named_Thms(val name: string val description: string): NAMED_THMS =
    27.9  struct
   27.10  
   27.11  structure Data = GenericDataFun
    28.1 --- a/src/Pure/axclass.ML	Thu Jul 02 21:24:32 2009 +0200
    28.2 +++ b/src/Pure/axclass.ML	Thu Jul 02 22:18:02 2009 +0200
    28.3 @@ -580,7 +580,7 @@
    28.4                | T as TVar (_, S) => insert (eq_fst op =) (T, S)
    28.5                | _ => I) typ [];
    28.6          val hyps = vars
    28.7 -          |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
    28.8 +          |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
    28.9          val ths = (typ, sort)
   28.10            |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
   28.11             {class_relation =
    29.1 --- a/src/Pure/drule.ML	Thu Jul 02 21:24:32 2009 +0200
    29.2 +++ b/src/Pure/drule.ML	Thu Jul 02 22:18:02 2009 +0200
    29.3 @@ -108,7 +108,6 @@
    29.4    val dummy_thm: thm
    29.5    val sort_constraintI: thm
    29.6    val sort_constraint_eq: thm
    29.7 -  val sort_triv: theory -> typ * sort -> thm list
    29.8    val unconstrainTs: thm -> thm
    29.9    val with_subgoal: int -> (thm -> thm) -> thm -> thm
   29.10    val comp_no_flatten: thm * int -> int -> thm -> thm
   29.11 @@ -209,15 +208,6 @@
   29.12  
   29.13  (* type classes and sorts *)
   29.14  
   29.15 -fun sort_triv thy (T, S) =
   29.16 -  let
   29.17 -    val certT = Thm.ctyp_of thy;
   29.18 -    val cT = certT T;
   29.19 -    fun class_triv c =
   29.20 -      Thm.class_triv thy c
   29.21 -      |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
   29.22 -  in map class_triv S end;
   29.23 -
   29.24  fun unconstrainTs th =
   29.25    fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar)
   29.26      (Thm.fold_terms Term.add_tvars th []) th;
    30.1 --- a/src/Pure/more_thm.ML	Thu Jul 02 21:24:32 2009 +0200
    30.2 +++ b/src/Pure/more_thm.ML	Thu Jul 02 22:18:02 2009 +0200
    30.3 @@ -26,6 +26,7 @@
    30.4    val eq_thm_thy: thm * thm -> bool
    30.5    val eq_thm_prop: thm * thm -> bool
    30.6    val equiv_thm: thm * thm -> bool
    30.7 +  val sort_triv: theory -> typ * sort -> thm list
    30.8    val check_shyps: sort list -> thm -> thm
    30.9    val is_dummy: thm -> bool
   30.10    val plain_prop_of: thm -> term
   30.11 @@ -168,7 +169,16 @@
   30.12    Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
   30.13  
   30.14  
   30.15 -(* sort hypotheses *)
   30.16 +(* type classes and sorts *)
   30.17 +
   30.18 +fun sort_triv thy (T, S) =
   30.19 +  let
   30.20 +    val certT = Thm.ctyp_of thy;
   30.21 +    val cT = certT T;
   30.22 +    fun class_triv c =
   30.23 +      Thm.class_triv thy c
   30.24 +      |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
   30.25 +  in map class_triv S end;
   30.26  
   30.27  fun check_shyps sorts raw_th =
   30.28    let
    31.1 --- a/src/Pure/proofterm.ML	Thu Jul 02 21:24:32 2009 +0200
    31.2 +++ b/src/Pure/proofterm.ML	Thu Jul 02 22:18:02 2009 +0200
    31.3 @@ -19,6 +19,7 @@
    31.4     | op %% of proof * proof
    31.5     | Hyp of term
    31.6     | PAxm of string * term * typ list option
    31.7 +   | Inclass of typ * class
    31.8     | Oracle of string * term * typ list option
    31.9     | Promise of serial * term * typ list
   31.10     | PThm of serial * ((string * term * typ list option) * proof_body future)
   31.11 @@ -140,6 +141,7 @@
   31.12   | op %% of proof * proof
   31.13   | Hyp of term
   31.14   | PAxm of string * term * typ list option
   31.15 + | Inclass of typ * class
   31.16   | Oracle of string * term * typ list option
   31.17   | Promise of serial * term * typ list
   31.18   | PThm of serial * ((string * term * typ list option) * proof_body future)
   31.19 @@ -290,6 +292,7 @@
   31.20        | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2
   31.21            handle SAME => prf1 %% mapp prf2)
   31.22        | mapp (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (map_typs Ts))
   31.23 +      | mapp (Inclass (T, c)) = Inclass (apsome g (SOME T) |> the, c)
   31.24        | mapp (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (map_typs Ts))
   31.25        | mapp (Promise (i, prop, Ts)) = Promise (i, prop, map_typs Ts)
   31.26        | mapp (PThm (i, ((a, prop, SOME Ts), body))) =
   31.27 @@ -317,6 +320,7 @@
   31.28    | fold_proof_terms f g (prf1 %% prf2) =
   31.29        fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
   31.30    | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
   31.31 +  | fold_proof_terms _ g (Inclass (T, _)) = g T
   31.32    | fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts
   31.33    | fold_proof_terms _ g (Promise (_, _, Ts)) = fold g Ts
   31.34    | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts
   31.35 @@ -331,6 +335,7 @@
   31.36    | size_of_proof _ = 1;
   31.37  
   31.38  fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
   31.39 +  | change_type (SOME [T]) (Inclass (_, c)) = Inclass (T, c)
   31.40    | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
   31.41    | change_type opTs (Promise _) = error "change_type: unexpected promise"
   31.42    | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body))
   31.43 @@ -468,6 +473,7 @@
   31.44        | norm (prf1 %% prf2) = (norm prf1 %% normh prf2
   31.45            handle SAME => prf1 %% norm prf2)
   31.46        | norm (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (htypeTs norm_types_same) Ts)
   31.47 +      | norm (Inclass (T, c)) = Inclass (htypeT norm_type_same T, c)
   31.48        | norm (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (htypeTs norm_types_same) Ts)
   31.49        | norm (Promise (i, prop, Ts)) = Promise (i, prop, htypeTs norm_types_same Ts)
   31.50        | norm (PThm (i, ((s, t, Ts), body))) =
   31.51 @@ -713,6 +719,8 @@
   31.52            handle SAME => prf1 %% lift' Us Ts prf2)
   31.53        | lift' _ _ (PAxm (s, prop, Ts)) =
   31.54            PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
   31.55 +      | lift' _ _ (Inclass (T, c)) =
   31.56 +          Inclass (same (op =) (Logic.incr_tvar inc) T, c)
   31.57        | lift' _ _ (Oracle (s, prop, Ts)) =
   31.58            Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
   31.59        | lift' _ _ (Promise (i, prop, Ts)) =
   31.60 @@ -967,8 +975,9 @@
   31.61               orelse has_duplicates (op =)
   31.62                 (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
   31.63               orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
   31.64 -      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp t)
   31.65 -      | shrink' ls lev ts prfs MinProof = ([], false, map (pair false) ts, MinProof)
   31.66 +      | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
   31.67 +      | shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf)
   31.68 +      | shrink' ls lev ts prfs (prf as Inclass _) = ([], false, map (pair false) ts, prf)
   31.69        | shrink' ls lev ts prfs prf =
   31.70            let
   31.71              val prop =
   31.72 @@ -1060,6 +1069,9 @@
   31.73        | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
   31.74            if s1 = s2 then optmatch matchTs inst (opTs, opUs)
   31.75            else raise PMatch
   31.76 +      | mtch Ts i j inst (Inclass (T1, c1), Inclass (T2, c2)) =
   31.77 +          if c1 = c2 then matchT inst (T1, T2)
   31.78 +          else raise PMatch
   31.79        | mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) =
   31.80            if name1 = name2 andalso prop1 = prop2 then
   31.81              optmatch matchTs inst (opTs, opUs)
   31.82 @@ -1091,6 +1103,7 @@
   31.83            NONE => prf
   31.84          | SOME prf' => incr_pboundvars plev tlev prf')
   31.85        | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Option.map (map substT) Ts)
   31.86 +      | subst _ _ (Inclass (T, c)) = Inclass (substT T, c)
   31.87        | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Option.map (map substT) Ts)
   31.88        | subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, (map substT) Ts)
   31.89        | subst _ _ (PThm (i, ((id, prop, Ts), body))) =
   31.90 @@ -1117,6 +1130,7 @@
   31.91          (_, Hyp (Var _)) => true
   31.92        | (Hyp (Var _), _) => true
   31.93        | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
   31.94 +      | (Inclass (_, c), Inclass (_, d)) => c = d andalso matchrands prf1 prf2
   31.95        | (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) =>
   31.96            a = b andalso propa = propb andalso matchrands prf1 prf2
   31.97        | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
    32.1 --- a/src/Pure/thm.ML	Thu Jul 02 21:24:32 2009 +0200
    32.2 +++ b/src/Pure/thm.ML	Thu Jul 02 22:18:02 2009 +0200
    32.3 @@ -487,7 +487,8 @@
    32.4          val extra' =
    32.5            Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra
    32.6            |> Sorts.minimal_sorts (Sign.classes_of thy);
    32.7 -        val shyps' = Sorts.union present extra';
    32.8 +        val shyps' = Sorts.union present extra'
    32.9 +          |> Sorts.remove_sort [];
   32.10        in
   32.11          Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
   32.12            shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
   32.13 @@ -1110,15 +1111,21 @@
   32.14        prop = Logic.mk_implies (A, A)});
   32.15  
   32.16  (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
   32.17 -fun class_triv thy c =
   32.18 +fun class_triv thy raw_c =
   32.19    let
   32.20 -    val Cterm {t, maxidx, sorts, ...} =
   32.21 -      cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
   32.22 -        handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   32.23 -    val der = deriv_rule0 (Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
   32.24 +    val c = Sign.certify_class thy raw_c;
   32.25 +    val T = TVar ((Name.aT, 0), [c]);
   32.26 +    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (T, c))
   32.27 +      handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   32.28    in
   32.29 -    Thm (der, {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx,
   32.30 -      shyps = sorts, hyps = [], tpairs = [], prop = t})
   32.31 +    Thm (deriv_rule0 (Pt.Inclass (T, c)),
   32.32 +     {thy_ref = Theory.check_thy thy,
   32.33 +      tags = [],
   32.34 +      maxidx = maxidx,
   32.35 +      shyps = sorts,
   32.36 +      hyps = [],
   32.37 +      tpairs = [],
   32.38 +      prop = prop})
   32.39    end;
   32.40  
   32.41  (*Internalize sort constraints of type variable*)
    33.1 --- a/src/Tools/atomize_elim.ML	Thu Jul 02 21:24:32 2009 +0200
    33.2 +++ b/src/Tools/atomize_elim.ML	Thu Jul 02 22:18:02 2009 +0200
    33.3 @@ -20,7 +20,9 @@
    33.4  struct
    33.5  
    33.6  (* theory data *)
    33.7 -structure AtomizeElimData = NamedThmsFun(
    33.8 +
    33.9 +structure AtomizeElimData = Named_Thms
   33.10 +(
   33.11    val name = "atomize_elim";
   33.12    val description = "atomize_elim rewrite rule";
   33.13  );
    34.1 --- a/src/ZF/UNITY/Constrains.thy	Thu Jul 02 21:24:32 2009 +0200
    34.2 +++ b/src/ZF/UNITY/Constrains.thy	Thu Jul 02 22:18:02 2009 +0200
    34.3 @@ -462,7 +462,11 @@
    34.4  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
    34.5  
    34.6  (*To allow expansion of the program's definition when appropriate*)
    34.7 -structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions");
    34.8 +structure Program_Defs = Named_Thms
    34.9 +(
   34.10 +  val name = "program"
   34.11 +  val description = "program definitions"
   34.12 +);
   34.13  
   34.14  (*proves "co" properties when the program is specified*)
   34.15  
   34.16 @@ -478,7 +482,7 @@
   34.17                (* Three subgoals *)
   34.18                rewrite_goal_tac [@{thm st_set_def}] 3,
   34.19                REPEAT (force_tac css 2),
   34.20 -              full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1,
   34.21 +              full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
   34.22                ALLGOALS (clarify_tac cs),
   34.23                REPEAT (FIRSTGOAL (etac disjE)),
   34.24                ALLGOALS (clarify_tac cs),
   34.25 @@ -493,7 +497,7 @@
   34.26      rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
   34.27  *}
   34.28  
   34.29 -setup ProgramDefs.setup
   34.30 +setup Program_Defs.setup
   34.31  
   34.32  method_setup safety = {*
   34.33    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
    35.1 --- a/src/ZF/UNITY/SubstAx.thy	Thu Jul 02 21:24:32 2009 +0200
    35.2 +++ b/src/ZF/UNITY/SubstAx.thy	Thu Jul 02 22:18:02 2009 +0200
    35.3 @@ -359,7 +359,7 @@
    35.4                    REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    35.5                                      @{thm EnsuresI}, @{thm ensuresI}] 1),
    35.6                (*now there are two subgoals: co & transient*)
    35.7 -              simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
    35.8 +              simp_tac (ss addsimps (Program_Defs.get ctxt)) 2,
    35.9                res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
   35.10                   (*simplify the command's domain*)
   35.11                simp_tac (ss addsimps [@{thm domain_def}]) 3,