# HG changeset patch
# User blanchet
# Date 1234179096 -3600
# Node ID 787349bb53e9309a1ec03b83062f990eeca186e2
# Parent  0abd89253a0fc123b880e13a15f6ac95d0d107c1
Reintroduced nitpick_ind_intro attribute.
It looks like I need it nonetheless.

diff -r 0abd89253a0f -r 787349bb53e9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Feb 09 10:39:57 2009 +0100
+++ b/src/HOL/HOL.thy	Mon Feb 09 12:31:36 2009 +0100
@@ -1714,9 +1714,15 @@
   val name = "nitpick_const_psimp"
   val description = "Partial equational specification of constants as needed by Nitpick"
 )
+structure Nitpick_Ind_Intro_Thms = NamedThmsFun
+(
+  val name = "nitpick_ind_intro"
+  val description = "Introduction rules for (co)inductive predicates as needed by Nitpick"
+)
 *}
 setup {* Nitpick_Const_Simp_Thms.setup
-         #> Nitpick_Const_Psimp_Thms.setup *}
+         #> Nitpick_Const_Psimp_Thms.setup
+         #> Nitpick_Ind_Intro_Thms.setup *}
 
 subsection {* Legacy tactics and ML bindings *}
 
diff -r 0abd89253a0f -r 787349bb53e9 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon Feb 09 10:39:57 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Mon Feb 09 12:31:36 2009 +0100
@@ -691,7 +691,8 @@
       ctxt |>
       LocalTheory.notes kind
         (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
-           [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
+           [Attrib.internal (K (ContextRules.intro_query NONE)),
+            Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>