# HG changeset patch
# User kleing
# Date 1114646235 -7200
# Node ID f011452b2815bdce2e53dea169c4bc8290d7cf23
# Parent  222092a48131727823989ec6fcde842c53511ba0
sped up a bit

diff -r 222092a48131 -r f011452b2815 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Apr 27 23:04:50 2005 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Apr 28 01:57:15 2005 +0200
@@ -6,7 +6,7 @@
 (* Compiler correctness statement and proof *)
 
 theory CorrComp
-imports "../J/JTypeSafe" "../Comp/LemmasComp"
+imports "../J/JTypeSafe" "LemmasComp"
 begin
 
 declare wf_prog_ws_prog [simp add]
@@ -1147,11 +1147,10 @@
 apply (rule_tac ?instrs0.0 = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
 apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
 apply (simp (no_asm_simp))
-apply (simp only: gh_conv)
-apply ((drule mp [OF _ TrueI])+, (drule spec)+)
-apply ((drule mp, assumption)+, assumption)
-  --{*extremely slow with Poly/ML (72s) and (under some circumstances)
-      unbearably slow with SML/NJ (up to 83 minutes)*}
+apply (simp only: gh_conv) 
+apply (drule mp [OF _ TrueI])+
+apply (erule allE, erule allE, erule allE, erule impE, assumption)+
+apply ((erule impE, assumption)+, assumption)
 
 apply (simp (no_asm_use))
 apply (simp (no_asm_simp) add: gmb_def)