diff -r b85c62c4e826 -r 6003b4f916c0 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Mon Feb 25 11:27:07 2002 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy	Mon Feb 25 18:02:22 2002 +0100
@@ -285,7 +285,7 @@
 
 lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl M) Z}"
 apply (unfold MGT_def)
-apply (rule_tac 'a = state in Impl1')
+apply (rule Impl1')
 apply  (rule_tac [2] UNIV_I)
 apply clarsimp
 apply (rule hoare_ehoare.ConjI)