--- a/src/HOL/Tools/inductive_package.ML Fri Feb 06 16:00:05 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Mon Feb 09 10:37:59 2009 +0100
@@ -691,8 +691,7 @@
ctxt |>
LocalTheory.notes kind
(map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
- [Attrib.internal (K (ContextRules.intro_query NONE)),
- Attrib.internal (K Nitpick_Ind_Intros_Thms.add)])]) intrs) |>>
+ [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), ctxt2) =
ctxt1 |>