# HG changeset patch
# User paulson
# Date 1032515346 -7200
# Node ID 1681c5b58766a95175b896c02c8609db3e9afd86
# Parent  d76a798281f44d1f4eb2f259fd272aa3146a9a1b
got rid of deepen_tac

diff -r d76a798281f4 -r 1681c5b58766 src/HOL/GroupTheory/Sylow.ML
--- a/src/HOL/GroupTheory/Sylow.ML	Fri Sep 20 11:48:35 2002 +0200
+++ b/src/HOL/GroupTheory/Sylow.ML	Fri Sep 20 11:49:06 2002 +0200
@@ -267,9 +267,9 @@
 
 Goal "(%C:{*H*}. M1 #> (@g. g \\<in> (G .<cr>) \\<and> H #> g = C)) \\<in> {* H *} \\<rightarrow> M";
 by (simp_tac (simpset() addsimps [setrcos_eq]) 1);
-by (deepen_tac (claset() addIs [someI2] 
+by (fast_tac (claset() addIs [someI2] 
             addSIs [restrictI, RelM_equiv, M_in_quot,
-                    M1_RelM_rcosetGM1g RSN (4, EquivElemClass),M1_in_M]) 0 1); 
+                    [RelM_equiv,M_in_quot,asm_rl,M1_RelM_rcosetGM1g] MRS EquivElemClass, M1_in_M]) 1);
 qed "setrcos_H_funcset_M";
 
 Goal "\\<exists>g \\<in> {* H *}\\<rightarrow>M. inj_on g ({* H *})";