# HG changeset patch
# User paulson
# Date 861610360 -7200
# Node ID 84df3b150b67c0d7bdc2782aa361de25988163c5
# Parent  3bb5d1b9c3aa2f943fd3a264201196c716bcc36e
Disabled the attempts for mutual induction to work so that single induction
involving sum types can work

diff -r 3bb5d1b9c3aa -r 84df3b150b67 src/HOL/add_ind_def.ML
--- a/src/HOL/add_ind_def.ML	Fri Apr 18 17:33:26 1997 +0200
+++ b/src/HOL/add_ind_def.ML	Mon Apr 21 10:12:40 1997 +0200
@@ -91,14 +91,11 @@
     val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
 
     (*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;
+    val dom_set  = body_type recT
+    val dom_sumT = dest_setT dom_set
 
     val freez   = Free(z, dom_sumT)
     and freeX   = Free(X, dom_set);
-    (*type of w may be any of the domTs*)
 
     fun dest_tprop (Const("Trueprop",_) $ P) = P
       | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
@@ -120,10 +117,11 @@
                   Const("Part", [dom_set, domT-->dom_sumT]---> dom_set)
           in  Part_const $ freeX $ Abs(w,domT,goodh)  end;
 
-    (*Access to balanced disjoint sums via injections*)
+    (*Access to balanced disjoint sums via injections??
+      Mutual recursion is NOT supported*)
     val parts = ListPair.map mk_Part
-                (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs),
-                 domTs);
+                (accesses_bal (ap Inl, ap Inr, Bound 0) 1,
+                 [dom_set]);
 
     (*replace each set by the corresponding Part(A,h)*)
     val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;