# HG changeset patch
# User blanchet
# Date 1234172279 -3600
# Node ID 6e93ae65c678532ba4b6c279f37b1c0cff03aa09
# Parent  c9bef39be3d275c341679e83361b985e65c65dea
Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
This should now be all.

diff -r c9bef39be3d2 -r 6e93ae65c678 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Feb 06 16:00:05 2009 +0100
+++ b/src/HOL/HOL.thy	Mon Feb 09 10:37:59 2009 +0100
@@ -1704,19 +1704,19 @@
 subsection {* Nitpick theorem store *}
 
 ML {*
-structure Nitpick_Const_Simps_Thms = NamedThmsFun
+structure Nitpick_Const_Simp_Thms = NamedThmsFun
 (
-  val name = "nitpick_const_simps"
+  val name = "nitpick_const_simp"
   val description = "Equational specification of constants as needed by Nitpick"
 )
-structure Nitpick_Ind_Intros_Thms = NamedThmsFun
+structure Nitpick_Const_Psimp_Thms = NamedThmsFun
 (
-  val name = "nitpick_ind_intros"
-  val description = "Introduction rules for inductive predicate as needed by Nitpick"
+  val name = "nitpick_const_psimp"
+  val description = "Partial equational specification of constants as needed by Nitpick"
 )
 *}
-setup {* Nitpick_Const_Simps_Thms.setup
-         o Nitpick_Ind_Intros_Thms.setup *}
+setup {* Nitpick_Const_Simp_Thms.setup
+         #> Nitpick_Const_Psimp_Thms.setup *}
 
 subsection {* Legacy tactics and ML bindings *}
 
diff -r c9bef39be3d2 -r 6e93ae65c678 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Feb 06 16:00:05 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 09 10:37:59 2009 +0100
@@ -333,9 +333,10 @@
     val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
       (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
           (DatatypeProp.make_cases new_type_names descr sorts thy2)
-
   in
     thy2
+    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
+       o Context.Theory
     |> parent_path flat_names
     |> store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
diff -r c9bef39be3d2 -r 6e93ae65c678 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Feb 06 16:00:05 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 09 10:37:59 2009 +0100
@@ -42,8 +42,7 @@
 
 fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
     let
-      val atts = Attrib.internal (K Simplifier.simp_add) ::
-                 Attrib.internal (K Nitpick_Const_Simps_Thms.add) :: moreatts
+      val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
       val spec = post simps
                    |> map (apfst (apsnd (append atts)))
                    |> map (apfst (apfst extra_qualify))
@@ -72,8 +71,9 @@
 
       val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
-            |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps
-            ||> fold_option (snd oo addsmps I "simps" []) trsimps
+            |> addsmps (NameSpace.qualified "partial") "psimps"
+                       [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
+            ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
             ||>> note_theorem ((qualify "pinduct",
                    [Attrib.internal (K (RuleCases.case_names cnames)),
                     Attrib.internal (K (RuleCases.consumes 1)),
@@ -128,7 +128,8 @@
       val tinduct = map remove_domain_condition pinducts
 
       val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
-      val allatts = if has_guards then [] else [Code.add_default_eqn_attrib]
+      val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
+        [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
 
       val qualify = NameSpace.qualified defname;
     in
diff -r c9bef39be3d2 -r 6e93ae65c678 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Fri Feb 06 16:00:05 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Mon Feb 09 10:37:59 2009 +0100
@@ -209,7 +209,7 @@
 
     val ([size_thms], thy'') =  PureThy.add_thmss
       [((Binding.name "size", size_eqns),
-        [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add,
+        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
          Thm.declaration_attribute
              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
 
@@ -239,4 +239,4 @@
 
 val setup = DatatypePackage.interpretation add_size_thms;
 
-end;
\ No newline at end of file
+end;
diff -r c9bef39be3d2 -r 6e93ae65c678 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Feb 06 16:00:05 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Mon Feb 09 10:37:59 2009 +0100
@@ -691,8 +691,7 @@
       ctxt |>
       LocalTheory.notes kind
         (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
-           [Attrib.internal (K (ContextRules.intro_query NONE)),
-            Attrib.internal (K Nitpick_Ind_Intros_Thms.add)])]) intrs) |>>
+           [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>
diff -r c9bef39be3d2 -r 6e93ae65c678 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Feb 06 16:00:05 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Mon Feb 09 10:37:59 2009 +0100
@@ -252,7 +252,7 @@
     val spec' = (map o apfst)
       (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
     val simp_atts = map (Attrib.internal o K)
-      [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add];
+      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())