diff -r 7d0fbdc46e8e -r 01beef6262aa src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Tue May 07 18:14:39 1996 +0200
+++ b/src/HOL/indrule.ML	Tue May 07 18:15:51 1996 +0200
@@ -99,23 +99,26 @@
 (*** Prove the simultaneous induction rule ***)
 
 (*Make distinct predicates for each inductive set.
-  Splits cartesian products in elem_type, IF nested to the right! *)
+  Splits cartesian products in elem_type, however nested*)
+
+(*The components of the element type, several if it is a product*)
+val elem_factors = Ind_Syntax.factors elem_type;
+val elem_frees = mk_frees "za" elem_factors;
+val elem_tuple = Ind_Syntax.mk_tuple elem_type elem_frees;
 
 (*Given a recursive set, return the "split" predicate
   and a conclusion for the simultaneous induction rule*)
 fun mk_predpair rec_tm = 
   let val rec_name = (#1 o dest_Const o head_of) rec_tm
-      val T = Ind_Syntax.factors elem_type ---> Ind_Syntax.boolT
-      val pfree = Free(pred_name ^ "_" ^ rec_name, T)
-      val frees = mk_frees "za" (binder_types T)
+      val pfree = Free(pred_name ^ "_" ^ rec_name, 
+		       elem_factors ---> Ind_Syntax.boolT)
       val qconcl = 
         foldr Ind_Syntax.mk_all 
-          (frees, 
-           Ind_Syntax.imp $ (Ind_Syntax.mk_mem 
-                             (foldr1 Ind_Syntax.mk_Pair frees, rec_tm))
-                $ (list_comb (pfree,frees)))
-  in  (Ind_Syntax.ap_split Ind_Syntax.boolT pfree (binder_types T), 
-      qconcl)  
+          (elem_frees, 
+           Ind_Syntax.imp $ (Ind_Syntax.mk_mem (elem_tuple, rec_tm))
+                $ (list_comb (pfree, elem_frees)))
+  in  (Ind_Syntax.ap_split elem_type Ind_Syntax.boolT pfree, 
+       qconcl)  
   end;
 
 val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
@@ -135,15 +138,18 @@
 and mutual_induct_concl = 
     Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
 
+val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
+			resolve_tac [allI, impI, conjI, Part_eqI, refl],
+			dresolve_tac [spec, mp, splitD]];
+
 val lemma = (*makes the link between the two induction rules*)
     prove_goalw_cterm part_rec_defs 
           (cterm_of sign (Logic.mk_implies (induct_concl,
                                             mutual_induct_concl)))
           (fn prems =>
            [cut_facts_tac prems 1,
-            REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
-             ORELSE resolve_tac [allI, impI, conjI, Part_eqI, refl] 1
-             ORELSE dresolve_tac [spec, mp, splitD] 1)])
+            REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN
+		    lemma_tac 1)])
     handle e => print_sign_exn sign e;
 
 (*Mutual induction follows by freeness of Inl/Inr.*)
@@ -151,9 +157,9 @@
 (*Simplification largely reduces the mutual induction rule to the 
   standard rule*)
 val mut_ss = simpset_of "Fun"
-             addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
+             addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];
 
-val all_defs = Inductive.con_defs @ part_rec_defs;
+val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;
 
 (*Removes Collects caused by M-operators in the intro rules*)
 val cmonos = [subset_refl RS Int_Collect_mono] RL Inductive.monos RLN
@@ -172,7 +178,7 @@
            simp_tac (mut_ss addsimps [Part_def]) 1  THEN
            IF_UNSOLVED (*simp_tac may have finished it off!*)
              ((*simplify assumptions, but don't accept new rewrite rules!*)
-              asm_full_simp_tac (mut_ss setmksimps K[]) 1  THEN
+              full_simp_tac mut_ss 1  THEN
               (*unpackage and use "prem" in the corresponding place*)
               REPEAT (rtac impI 1)  THEN
               rtac (rewrite_rule all_defs prem) 1  THEN
@@ -195,23 +201,27 @@
             mutual_ind_tac (rev prems) (length prems)])
     handle e => print_sign_exn sign e;
 
-(*Attempts to remove all occurrences of split*)
-val split_tac =
-    REPEAT (SOMEGOAL (FIRST' [rtac splitI, 
-                              dtac splitD,
-                              etac splitE,
-                              bound_hyp_subst_tac]))
-    THEN prune_params_tac;
+(** Uncurrying the predicate in the ordinary induction rule **)
+
+(*The name "x.1" comes from the "RS spec" !*)
+val xvar = cterm_of sign (Var(("x",1), elem_type));
+
+(*strip quantifier and instantiate the variable to a tuple*)
+val induct0 = quant_induct RS spec RSN (2,rev_mp) |>
+              freezeT |>     (*Because elem_type contains TFrees not TVars*)
+              instantiate ([], [(xvar, cterm_of sign elem_tuple)]);
 
 in
   struct
-  (*strip quantifier*)
-  val induct = standard (quant_induct RS spec RSN (2,rev_mp));
+  val induct = standard 
+                  (Ind_Syntax.split_rule_var
+		    (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
+		     induct0));
 
+  (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   val mutual_induct = 
-      if length Intr_elim.rec_names > 1 orelse
-         length (Ind_Syntax.factors elem_type) > 1
-      then rule_by_tactic split_tac mutual_induct_split
+      if length Intr_elim.rec_names > 1
+      then Ind_Syntax.remove_split mutual_induct_split
       else TrueI;
   end
 end;