src/HOL/Tools/inductive_set.ML
changeset 35646 b32d6c1bdb4d
parent 35364 b8c62d60195c
child 35757 c2884bec5463
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Mar 08 09:38:59 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Mar 08 15:00:34 2010 +0100
     1.3 @@ -520,7 +520,7 @@
     1.4      val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
     1.5      val (intr_names, intr_atts) = split_list (map fst intros);
     1.6      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     1.7 -    val (intrs', elims', induct, lthy4) =
     1.8 +    val (intrs', elims', induct, inducts, lthy4) =
     1.9        Inductive.declare_rules rec_name coind no_ind cnames
    1.10          (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    1.11          (map (fn th => (to_set [] (Context.Proof lthy3) th,
    1.12 @@ -528,7 +528,7 @@
    1.13             Rule_Cases.get_constraints th)) elims)
    1.14          raw_induct' lthy3;
    1.15    in
    1.16 -    ({intrs = intrs', elims = elims', induct = induct,
    1.17 +    ({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
    1.18        raw_induct = raw_induct', preds = map fst defs},
    1.19       lthy4)
    1.20    end;