1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 15:37:14 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 15:38:47 2010 +0200
     1.3 @@ -1674,10 +1674,14 @@
     1.4    map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
     1.5    |> const_nondef_table
     1.6  fun inductive_intro_table ctxt subst def_table =
     1.7 -  def_table_for
     1.8 -      (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
     1.9 -                                            def_table o prop_of)
    1.10 -           o Nitpick_Intros.get) ctxt subst
    1.11 +  let val thy = ProofContext.theory_of ctxt in
    1.12 +    def_table_for
    1.13 +        (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
    1.14 +               o snd o snd)
    1.15 +         o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
    1.16 +                                  cat = Spec_Rules.Co_Inductive)
    1.17 +         o Spec_Rules.get) ctxt subst
    1.18 +  end
    1.19  fun ground_theorem_table thy =
    1.20    fold ((fn @{const Trueprop} $ t1 =>
    1.21              is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)