src/HOL/Tools/inductive_set.ML
changeset 35757 c2884bec5463
parent 35646 b32d6c1bdb4d
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Mar 12 12:14:30 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 12 12:14:31 2010 +0100
     1.3 @@ -521,7 +521,7 @@
     1.4      val (intr_names, intr_atts) = split_list (map fst intros);
     1.5      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     1.6      val (intrs', elims', induct, inducts, lthy4) =
     1.7 -      Inductive.declare_rules rec_name coind no_ind cnames
     1.8 +      Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
     1.9          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    1.10          (map (fn th => (to_set [] (Context.Proof lthy3) th,
    1.11             map fst (fst (Rule_Cases.get th)),