# HG changeset patch
# User paulson
# Date 862400440 -7200
# Node ID a2de0be6e14d52b83bfc30187a357d64e97b9513
# Parent  f45074fab9c7dc63b05366cb3d43fc4fb2364e8b
No longer proves mutual induction rules unless they are needed

diff -r f45074fab9c7 -r a2de0be6e14d src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Wed Apr 30 13:39:56 1997 +0200
+++ b/src/HOL/indrule.ML	Wed Apr 30 13:40:40 1997 +0200
@@ -148,15 +148,20 @@
                         resolve_tac [allI, impI, conjI, Part_eqI, refl],
                         dresolve_tac [spec, mp, splitD]];
 
+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 [split RS eq_reflection] THEN
-                    lemma_tac 1)])
-    handle e => print_sign_exn sign e;
+  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 [split RS eq_reflection] THEN
+		    lemma_tac 1)])
+      handle e => print_sign_exn sign e)
+  else TrueI;
 
 (*Mutual induction follows by freeness of Inl/Inr.*)
 
@@ -193,9 +198,8 @@
           ) i)
        THEN mutual_ind_tac prems (i-1);
 
-val _ = writeln "  Proving the mutual induction rule...";
-
 val mutual_induct_split = 
+  if need_mutual then
     prove_goalw_cterm []
           (cterm_of sign
            (Logic.list_implies (map (induct_prem (Inductive.rec_tms ~~ preds)) 
@@ -204,7 +208,8 @@
           (fn prems =>
            [rtac (quant_induct RS lemma) 1,
             mutual_ind_tac (rev prems) (length prems)])
-    handle e => print_sign_exn sign e;
+    handle e => print_sign_exn sign e
+  else TrueI;
 
 (** Uncurrying the predicate in the ordinary induction rule **)
 
@@ -224,9 +229,6 @@
                      induct0));
 
   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
-  val mutual_induct = 
-      if length Intr_elim.rec_names > 1
-      then Prod_Syntax.remove_split mutual_induct_split
-      else TrueI;
+  val mutual_induct = Prod_Syntax.remove_split mutual_induct_split
   end
 end;