1.1 --- a/src/HOL/add_ind_def.ML	Fri Apr 18 17:33:26 1997 +0200
     1.2 +++ b/src/HOL/add_ind_def.ML	Mon Apr 21 10:12:40 1997 +0200
     1.3 @@ -91,14 +91,11 @@
     1.4      val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
     1.5  
     1.6      (*Mutual recursion ?? *)
     1.7 -    val domTs = summands (dest_setT (body_type recT));
     1.8 -                (*alternative defn: map (dest_setT o fastype_of) rec_tms *)
     1.9 -    val dom_sumT = fold_bal mk_sum domTs;
    1.10 -    val dom_set  = mk_setT dom_sumT;
    1.11 +    val dom_set  = body_type recT
    1.12 +    val dom_sumT = dest_setT dom_set
    1.13  
    1.14      val freez   = Free(z, dom_sumT)
    1.15      and freeX   = Free(X, dom_set);
    1.16 -    (*type of w may be any of the domTs*)
    1.17  
    1.18      fun dest_tprop (Const("Trueprop",_) $ P) = P
    1.19        | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
    1.20 @@ -120,10 +117,11 @@
    1.21                    Const("Part", [dom_set, domT-->dom_sumT]---> dom_set)
    1.22            in  Part_const $ freeX $ Abs(w,domT,goodh)  end;
    1.23  
    1.24 -    (*Access to balanced disjoint sums via injections*)
    1.25 +    (*Access to balanced disjoint sums via injections??
    1.26 +      Mutual recursion is NOT supported*)
    1.27      val parts = ListPair.map mk_Part
    1.28 -                (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs),
    1.29 -                 domTs);
    1.30 +                (accesses_bal (ap Inl, ap Inr, Bound 0) 1,
    1.31 +                 [dom_set]);
    1.32  
    1.33      (*replace each set by the corresponding Part(A,h)*)
    1.34      val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;