# HG changeset patch
# User paulson
# Date 862475290 -7200
# Node ID eeb4d0c7f7484c72f0a1b409a503e3608dfc978b
# Parent  32dad29d4666de8aac69b9ea9c53ab69db5485fa
No longer proves mutual_induct unless it is necessary.
Previous version proved it, then threw it away...

diff -r 32dad29d4666 -r eeb4d0c7f748 src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Wed Apr 30 16:36:59 1997 +0200
+++ b/src/ZF/indrule.ML	Thu May 01 10:28:10 1997 +0200
@@ -151,13 +151,19 @@
                         resolve_tac [allI, impI, conjI, Part_eqI],
                         dresolve_tac [spec, mp, Pr.fsplitD]];
 
+val need_mutual = length Intr_elim.rec_names > 1;
+
 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 (rewrite_goals_tac [Pr.split_eq] THEN
-                    lemma_tac 1)]);
+  if need_mutual then
+     (writeln "  Proving the mutual induction rule...";
+      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 (rewrite_goals_tac [Pr.split_eq] THEN
+		      lemma_tac 1)]))
+  else TrueI;
 
 (*Mutual induction follows by freeness of Inl/Inr.*)
 
@@ -203,9 +209,8 @@
           ) i)
        THEN mutual_ind_tac prems (i-1);
 
-val _ = writeln "  Proving the mutual induction rule...";
-
 val mutual_induct_fsplit = 
+  if need_mutual then
     prove_goalw_cterm []
           (cterm_of sign
            (Logic.list_implies 
@@ -213,9 +218,8 @@
                mutual_induct_concl)))
           (fn prems =>
            [rtac (quant_induct RS lemma) 1,
-            mutual_ind_tac (rev prems) (length prems)]);
-
-
+            mutual_ind_tac (rev prems) (length prems)])
+  else TrueI;
 
 (** Uncurrying the predicate in the ordinary induction rule **)
 
@@ -240,9 +244,6 @@
                      induct0));
 
   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
-  val mutual_induct = 
-      if length Intr_elim.rec_names > 1 
-      then CP.remove_split mutual_induct_fsplit
-      else TrueI;
+  val mutual_induct = CP.remove_split mutual_induct_fsplit
   end
 end;