--- a/src/HOL/add_ind_def.ML Tue Jul 25 16:59:08 1995 +0200
+++ b/src/HOL/add_ind_def.ML Tue Jul 25 17:00:15 1995 +0200
@@ -54,7 +54,7 @@
let
val sign = sign_of thy;
- (*recT and rec_params should agree for all mutually recursive components*)
+ (*rec_params should agree for all mutually recursive components*)
val rec_hds = map head_of rec_tms;
val _ = assert_all is_Const rec_hds
@@ -87,8 +87,9 @@
val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
- (*Probably INCORRECT for mutual recursion!*)
- val domTs = summands(dest_setT (body_type recT));
+ (*Mutual recursion ?? *)
+ val domTs = summands (dest_setT (body_type recT));
+ (*alternative defn: map (dest_setT o fastype_of) rec_tms *)
val dom_sumT = fold_bal mk_sum domTs;
val dom_set = mk_setT dom_sumT;