# HG changeset patch
# User lcp
# Date 785758435 -3600
# Node ID f0aacbcedb777f2ad6d39263091a37d23215d842
# Parent  019aadf0e3156dced34acda3067612436c9b5b99
ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any
equalities, by adding setmksimps K[].

ZF/indrule/mut_ss: removed Collect_cong; it is redundant.

diff -r 019aadf0e315 -r f0aacbcedb77 src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Fri Nov 25 11:08:12 1994 +0100
+++ b/src/ZF/indrule.ML	Fri Nov 25 11:13:55 1994 +0100
@@ -139,8 +139,7 @@
 (*Simplification largely reduces the mutual induction rule to the 
   standard rule*)
 val mut_ss = 
-    FOL_ss addcongs [Collect_cong]
-	   addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
+    FOL_ss addsimps   [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
 
 val all_defs = con_defs@part_rec_defs;
 
@@ -159,17 +158,19 @@
        (SELECT_GOAL 
 	  (
 	   (*Simplify the assumptions and goal by unfolding Part and
-	     using freeness of the Sum constructors*)
+	     using freeness of the Sum constructors; proves all but one
+             conjunct by contradiction*)
 	   rewrite_goals_tac all_defs  THEN
 	   simp_tac (mut_ss addsimps [Part_iff]) 1  THEN
 	   IF_UNSOLVED (*simp_tac may have finished it off!*)
-	     (asm_full_simp_tac mut_ss 1  THEN
+	     ((*simplify assumptions, but don't accept new rewrite rules!*)
+	      asm_full_simp_tac (mut_ss setmksimps K[]) 1  THEN
 	      (*unpackage and use "prem" in the corresponding place*)
 	      REPEAT (rtac impI 1)  THEN
 	      rtac (rewrite_rule all_defs prem) 1  THEN
 	      (*prem must not be REPEATed below: could loop!*)
 	      DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 
-			      eresolve_tac ([conjE]@cmonos))))
+				      eresolve_tac (conjE::mp::cmonos))))
 	  ) i)
        THEN mutual_ind_tac prems (i-1);