src/HOL/Tools/inductive.ML
changeset 31902 862ae16a799d
parent 31723 f5cafe803b55
child 31986 a68f88d264f7
     1.1 --- a/src/HOL/Tools/inductive.ML	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -694,7 +694,7 @@
     1.4        LocalTheory.notes kind
     1.5          (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
     1.6             [Attrib.internal (K (ContextRules.intro_query NONE)),
     1.7 -            Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>>
     1.8 +            Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
     1.9        map (hd o snd);
    1.10      val (((_, elims'), (_, [induct'])), ctxt2) =
    1.11        ctxt1 |>