src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Jul 02 17:34:14 2009 +0200
@@ -694,7 +694,7 @@
       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_Intro_Thms.add)])]) intrs) |>>
+            Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>