diff -r 15bee2731e43 -r 40d64cb4f4e6 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Mon Aug 07 14:32:56 2000 +0200
@@ -34,7 +34,7 @@
 	 in
          (\\<exists>rT maxl ins.
          method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and>
-	 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = (Invoke mn pTs) \\<and>
+	(\\<exists>C' mn pTs k. pc = k+1 \\<and> ins!k = (Invoke C' mn pTs) \\<and>
          (mn,pTs) = sig0 \\<and> 
          (\\<exists>apTs D ST'.
          fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>