# HG changeset patch
# User paulson
# Date 837435277 -7200
# Node ID 505b104f675a8c990f3109d7bc556918c9c20c1f
# Parent  71bfeecfa96c974a2ca0c93d3dd705b05c71742e
Uses minimal simpset (min_ss) and full_simp_tac
instead of asm_full_simp_tac to prevent excessive simplification, which
can cause proofs to fail

diff -r 71bfeecfa96c -r 505b104f675a src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Mon Jul 15 12:36:56 1996 +0200
+++ b/src/HOL/indrule.ML	Mon Jul 15 14:54:37 1996 +0200
@@ -81,6 +81,15 @@
 val _ = seq (writeln o Sign.string_of_term sign) ind_prems;
 *)
 
+(*We use a MINIMAL simpset because others (such as HOL_ss) contain too many
+  simplifications.  If the premises get simplified, then the proofs will 
+  fail.  This arose with a premise of the form {(F n,G n)|n . True}, which
+  expanded to something containing ...&True. *)
+val min_ss = empty_ss
+      setmksimps (mksimps mksimps_pairs)
+      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
+                             ORELSE' etac FalseE);
+
 val quant_induct = 
     prove_goalw_cterm part_rec_defs 
       (cterm_of sign 
@@ -90,7 +99,7 @@
       (fn prems =>
        [rtac (impI RS allI) 1,
         DETERM (etac Intr_elim.raw_induct 1),
-        asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1,
+        full_simp_tac (min_ss addsimps [Part_Collect]) 1,
         REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
                            ORELSE' hyp_subst_tac)),
         ind_tac (rev prems) (length prems)])
@@ -156,8 +165,7 @@
 
 (*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, split];
+val mut_ss = min_ss addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];
 
 val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;