1.1 --- a/src/HOL/HOL.thy	Fri Feb 06 16:00:05 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Feb 09 10:37:59 2009 +0100
     1.3 @@ -1704,19 +1704,19 @@
     1.4  subsection {* Nitpick theorem store *}
     1.5  
     1.6  ML {*
     1.7 -structure Nitpick_Const_Simps_Thms = NamedThmsFun
     1.8 +structure Nitpick_Const_Simp_Thms = NamedThmsFun
     1.9  (
    1.10 -  val name = "nitpick_const_simps"
    1.11 +  val name = "nitpick_const_simp"
    1.12    val description = "Equational specification of constants as needed by Nitpick"
    1.13  )
    1.14 -structure Nitpick_Ind_Intros_Thms = NamedThmsFun
    1.15 +structure Nitpick_Const_Psimp_Thms = NamedThmsFun
    1.16  (
    1.17 -  val name = "nitpick_ind_intros"
    1.18 -  val description = "Introduction rules for inductive predicate as needed by Nitpick"
    1.19 +  val name = "nitpick_const_psimp"
    1.20 +  val description = "Partial equational specification of constants as needed by Nitpick"
    1.21  )
    1.22  *}
    1.23 -setup {* Nitpick_Const_Simps_Thms.setup
    1.24 -         o Nitpick_Ind_Intros_Thms.setup *}
    1.25 +setup {* Nitpick_Const_Simp_Thms.setup
    1.26 +         #> Nitpick_Const_Psimp_Thms.setup *}
    1.27  
    1.28  subsection {* Legacy tactics and ML bindings *}
    1.29  

     2.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Feb 06 16:00:05 2009 +0100
     2.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 09 10:37:59 2009 +0100
     2.3 @@ -333,9 +333,10 @@
     2.4      val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
     2.5        (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
     2.6            (DatatypeProp.make_cases new_type_names descr sorts thy2)
     2.7 -
     2.8    in
     2.9      thy2
    2.10 +    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
    2.11 +       o Context.Theory
    2.12      |> parent_path flat_names
    2.13      |> store_thmss "cases" new_type_names case_thms
    2.14      |-> (fn thmss => pair (thmss, case_names))

     3.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Feb 06 16:00:05 2009 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 09 10:37:59 2009 +0100
     3.3 @@ -42,8 +42,7 @@
     3.4  
     3.5  fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
     3.6      let
     3.7 -      val atts = Attrib.internal (K Simplifier.simp_add) ::
     3.8 -                 Attrib.internal (K Nitpick_Const_Simps_Thms.add) :: moreatts
     3.9 +      val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
    3.10        val spec = post simps
    3.11                     |> map (apfst (apsnd (append atts)))
    3.12                     |> map (apfst (apfst extra_qualify))
    3.13 @@ -72,8 +71,9 @@
    3.14  
    3.15        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    3.16            lthy
    3.17 -            |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps
    3.18 -            ||> fold_option (snd oo addsmps I "simps" []) trsimps
    3.19 +            |> addsmps (NameSpace.qualified "partial") "psimps"
    3.20 +                       [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
    3.21 +            ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
    3.22              ||>> note_theorem ((qualify "pinduct",
    3.23                     [Attrib.internal (K (RuleCases.case_names cnames)),
    3.24                      Attrib.internal (K (RuleCases.consumes 1)),
    3.25 @@ -128,7 +128,8 @@
    3.26        val tinduct = map remove_domain_condition pinducts
    3.27  
    3.28        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
    3.29 -      val allatts = if has_guards then [] else [Code.add_default_eqn_attrib]
    3.30 +      val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
    3.31 +        [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
    3.32  
    3.33        val qualify = NameSpace.qualified defname;
    3.34      in

     4.1 --- a/src/HOL/Tools/function_package/size.ML	Fri Feb 06 16:00:05 2009 +0100
     4.2 +++ b/src/HOL/Tools/function_package/size.ML	Mon Feb 09 10:37:59 2009 +0100
     4.3 @@ -209,7 +209,7 @@
     4.4  
     4.5      val ([size_thms], thy'') =  PureThy.add_thmss
     4.6        [((Binding.name "size", size_eqns),
     4.7 -        [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add,
     4.8 +        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
     4.9           Thm.declaration_attribute
    4.10               (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
    4.11  
    4.12 @@ -239,4 +239,4 @@
    4.13  
    4.14  val setup = DatatypePackage.interpretation add_size_thms;
    4.15  
    4.16 -end;
    4.17 \ No newline at end of file
    4.18 +end;

     5.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Feb 06 16:00:05 2009 +0100
     5.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Feb 09 10:37:59 2009 +0100
     5.3 @@ -691,8 +691,7 @@
     5.4        ctxt |>
     5.5        LocalTheory.notes kind
     5.6          (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
     5.7 -           [Attrib.internal (K (ContextRules.intro_query NONE)),
     5.8 -            Attrib.internal (K Nitpick_Ind_Intros_Thms.add)])]) intrs) |>>
     5.9 +           [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
    5.10        map (hd o snd);
    5.11      val (((_, elims'), (_, [induct'])), ctxt2) =
    5.12        ctxt1 |>

     6.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Feb 06 16:00:05 2009 +0100
     6.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon Feb 09 10:37:59 2009 +0100
     6.3 @@ -252,7 +252,7 @@
     6.4      val spec' = (map o apfst)
     6.5        (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
     6.6      val simp_atts = map (Attrib.internal o K)
     6.7 -      [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add];
     6.8 +      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add];
     6.9    in
    6.10      lthy
    6.11      |> set_group ? LocalTheory.set_group (serial_string ())