# HG changeset patch
# User lcp
# Date 806684415 -7200
# Node ID c17a8fd0c95d64f97e6239222493433bdc383dd8
# Parent  0443e4dc8511b37e0d82a7953ce4efd25f3c097f
Changed comments

diff -r 0443e4dc8511 -r c17a8fd0c95d src/HOL/add_ind_def.ML
--- 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;