changeset 33056 | 791a4655cae3 |
parent 33051 | 3797ae7ffe3c |
child 33077 | 3c9cf88ec841 |
--- a/src/HOL/Tools/inductive.ML Wed Oct 21 16:57:57 2009 +0200 +++ b/src/HOL/Tools/inductive.ML Wed Oct 21 17:34:35 2009 +0200 @@ -703,7 +703,7 @@ LocalTheory.notes kind (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE)), - Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>> + Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>> map (hd o snd); val (((_, elims'), (_, [induct'])), ctxt2) = ctxt1 |>