--- a/src/HOL/Tools/inductive_set.ML Fri Mar 12 12:14:30 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML Fri Mar 12 12:14:31 2010 +0100
@@ -521,7 +521,7 @@
val (intr_names, intr_atts) = split_list (map fst intros);
val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
val (intrs', elims', induct, inducts, lthy4) =
- Inductive.declare_rules rec_name coind no_ind cnames
+ Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
(map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
(map (fn th => (to_set [] (Context.Proof lthy3) th,
map fst (fst (Rule_Cases.get th)),