1.1 --- a/NEWS	Tue Jun 01 15:37:14 2010 +0200
     1.2 +++ b/NEWS	Tue Jun 01 15:38:47 2010 +0200
     1.3 @@ -435,6 +435,7 @@
     1.4      "SAT4J_Light".  INCOMPATIBILITY.
     1.5    - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
     1.6      "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
     1.7 +  - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
     1.8  
     1.9  * Moved the SMT binding into the HOL image.
    1.10  

     2.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Jun 01 15:37:14 2010 +0200
     2.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Jun 01 15:38:47 2010 +0200
     2.3 @@ -2578,21 +2578,6 @@
     2.4  
     2.5  \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
     2.6  
     2.7 -\flushitem{\textit{nitpick\_intro}}
     2.8 -
     2.9 -\nopagebreak
    2.10 -This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
    2.11 -For predicates defined using the \textbf{inductive} or \textbf{coinductive}
    2.12 -command, this corresponds to the \textit{intros} rules. The introduction rules
    2.13 -must be of the form
    2.14 -
    2.15 -\qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
    2.16 -\ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk$ \\
    2.17 -\hbox{}\qquad ${\Longrightarrow}\;\, c\ u_1\ \ldots\ u_n$,
    2.18 -
    2.19 -where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
    2.20 -optional monotonic operator. The order of the assumptions is irrelevant.
    2.21 -
    2.22  \flushitem{\textit{nitpick\_choice\_spec}}
    2.23  
    2.24  \nopagebreak
    2.25 @@ -2641,9 +2626,8 @@
    2.26  ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
    2.27  \postw
    2.28  
    2.29 -Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
    2.30 -the above rules. Nitpick then uses the \textit{lfp}-based definition in
    2.31 -conjunction with these rules. To override this, we can specify an alternative
    2.32 +By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
    2.33 +the introduction rules. To override this, we can specify an alternative
    2.34  definition as follows:
    2.35  
    2.36  \prew

     3.1 --- a/src/HOL/HOL.thy	Tue Jun 01 15:37:14 2010 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue Jun 01 15:38:47 2010 +0200
     3.3 @@ -2033,11 +2033,6 @@
     3.4    val name = "nitpick_psimp"
     3.5    val description = "partial equational specification of constants as needed by Nitpick"
     3.6  )
     3.7 -structure Nitpick_Intros = Named_Thms
     3.8 -(
     3.9 -  val name = "nitpick_intro"
    3.10 -  val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    3.11 -)
    3.12  structure Nitpick_Choice_Specs = Named_Thms
    3.13  (
    3.14    val name = "nitpick_choice_spec"
    3.15 @@ -2049,7 +2044,6 @@
    3.16    Nitpick_Defs.setup
    3.17    #> Nitpick_Simps.setup
    3.18    #> Nitpick_Psimps.setup
    3.19 -  #> Nitpick_Intros.setup
    3.20    #> Nitpick_Choice_Specs.setup
    3.21  *}
    3.22  

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 15:37:14 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 15:38:47 2010 +0200
     4.3 @@ -1674,10 +1674,14 @@
     4.4    map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
     4.5    |> const_nondef_table
     4.6  fun inductive_intro_table ctxt subst def_table =
     4.7 -  def_table_for
     4.8 -      (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
     4.9 -                                            def_table o prop_of)
    4.10 -           o Nitpick_Intros.get) ctxt subst
    4.11 +  let val thy = ProofContext.theory_of ctxt in
    4.12 +    def_table_for
    4.13 +        (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
    4.14 +               o snd o snd)
    4.15 +         o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
    4.16 +                                  cat = Spec_Rules.Co_Inductive)
    4.17 +         o Spec_Rules.get) ctxt subst
    4.18 +  end
    4.19  fun ground_theorem_table thy =
    4.20    fold ((fn @{const Trueprop} $ t1 =>
    4.21              is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)

     5.1 --- a/src/HOL/Tools/inductive.ML	Tue Jun 01 15:37:14 2010 +0200
     5.2 +++ b/src/HOL/Tools/inductive.ML	Tue Jun 01 15:38:47 2010 +0200
     5.3 @@ -719,8 +719,7 @@
     5.4        Local_Theory.notes
     5.5          (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
     5.6            map (fn th => [([th],
     5.7 -           [Attrib.internal (K (Context_Rules.intro_query NONE)),
     5.8 -            Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
     5.9 +           [Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>>
    5.10        map (hd o snd);
    5.11      val (((_, elims'), (_, [induct'])), lthy2) =
    5.12        lthy1 |>