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 |>