diff -r cc0fd5226bb7 -r c32c5696ec2a src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Mon Jul 17 14:00:53 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 = MI(Invoke mn pTs) \\<and>
+	 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = (Invoke mn pTs) \\<and>
          (mn,pTs) = sig0 \\<and> 
          (\\<exists>apTs D ST'.
          fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>