# HG changeset patch
# User blanchet
# Date 1275399527 -7200
# Node ID 8b931fb51cc67854fe72816f411c245f1f123351
# Parent  54c15abf3b932b55774c4434e8f83bc3f636edf4
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead

diff -r 54c15abf3b93 -r 8b931fb51cc6 NEWS
--- a/NEWS	Tue Jun 01 15:37:14 2010 +0200
+++ b/NEWS	Tue Jun 01 15:38:47 2010 +0200
@@ -435,6 +435,7 @@
     "SAT4J_Light".  INCOMPATIBILITY.
   - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
     "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
+  - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
 
 * Moved the SMT binding into the HOL image.
 
diff -r 54c15abf3b93 -r 8b931fb51cc6 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Jun 01 15:37:14 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Tue Jun 01 15:38:47 2010 +0200
@@ -2578,21 +2578,6 @@
 
 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
 
-\flushitem{\textit{nitpick\_intro}}
-
-\nopagebreak
-This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
-For predicates defined using the \textbf{inductive} or \textbf{coinductive}
-command, this corresponds to the \textit{intros} rules. The introduction rules
-must be of the form
-
-\qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
-\ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk$ \\
-\hbox{}\qquad ${\Longrightarrow}\;\, c\ u_1\ \ldots\ u_n$,
-
-where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
-optional monotonic operator. The order of the assumptions is irrelevant.
-
 \flushitem{\textit{nitpick\_choice\_spec}}
 
 \nopagebreak
@@ -2641,9 +2626,8 @@
 ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
 \postw
 
-Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
-the above rules. Nitpick then uses the \textit{lfp}-based definition in
-conjunction with these rules. To override this, we can specify an alternative
+By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
+the introduction rules. To override this, we can specify an alternative
 definition as follows:
 
 \prew
diff -r 54c15abf3b93 -r 8b931fb51cc6 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 01 15:37:14 2010 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 01 15:38:47 2010 +0200
@@ -2033,11 +2033,6 @@
   val name = "nitpick_psimp"
   val description = "partial equational specification of constants as needed by Nitpick"
 )
-structure Nitpick_Intros = Named_Thms
-(
-  val name = "nitpick_intro"
-  val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
-)
 structure Nitpick_Choice_Specs = Named_Thms
 (
   val name = "nitpick_choice_spec"
@@ -2049,7 +2044,6 @@
   Nitpick_Defs.setup
   #> Nitpick_Simps.setup
   #> Nitpick_Psimps.setup
-  #> Nitpick_Intros.setup
   #> Nitpick_Choice_Specs.setup
 *}
 
diff -r 54c15abf3b93 -r 8b931fb51cc6 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 15:37:14 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 15:38:47 2010 +0200
@@ -1674,10 +1674,14 @@
   map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
   |> const_nondef_table
 fun inductive_intro_table ctxt subst def_table =
-  def_table_for
-      (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
-                                            def_table o prop_of)
-           o Nitpick_Intros.get) ctxt subst
+  let val thy = ProofContext.theory_of ctxt in
+    def_table_for
+        (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
+               o snd o snd)
+         o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
+                                  cat = Spec_Rules.Co_Inductive)
+         o Spec_Rules.get) ctxt subst
+  end
 fun ground_theorem_table thy =
   fold ((fn @{const Trueprop} $ t1 =>
             is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
diff -r 54c15abf3b93 -r 8b931fb51cc6 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Jun 01 15:37:14 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Jun 01 15:38:47 2010 +0200
@@ -719,8 +719,7 @@
       Local_Theory.notes
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
           map (fn th => [([th],
-           [Attrib.internal (K (Context_Rules.intro_query NONE)),
-            Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
+           [Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), lthy2) =
       lthy1 |>