src/HOL/Tools/inductive_set.ML
changeset 33459 a4a38ed813f7
parent 33458 ae1f5d89b082
child 33519 e31a85f92ce9
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Nov 05 22:59:57 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 05 23:59:23 2009 +0100
     1.3 @@ -520,10 +520,10 @@
     1.4      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     1.5      val (intrs', elims', induct, lthy4) =
     1.6        Inductive.declare_rules kind rec_name coind no_ind cnames
     1.7 -      (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
     1.8 -      (map (fn th => (to_set [] (Context.Proof lthy3) th,
     1.9 -         map fst (fst (Rule_Cases.get th)))) elims)
    1.10 -      raw_induct' lthy3
    1.11 +        (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    1.12 +        (map (fn th => (to_set [] (Context.Proof lthy3) th,
    1.13 +           map fst (fst (Rule_Cases.get th)))) elims)
    1.14 +        raw_induct' lthy3;
    1.15    in
    1.16      ({intrs = intrs', elims = elims', induct = induct,
    1.17        raw_induct = raw_induct', preds = map fst defs},