diff -r 40d64cb4f4e6 -r 19a6d1289f5e src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Mon Aug 07 14:32:56 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Mon Aug 07 14:34:03 2000 +0200
@@ -56,7 +56,7 @@
 	 in
       (xp', hp, (stk', vars, Cl, sig, pc+1)#frs))"
 
- "exec_instr (Invoke mn ps) G hp stk vars Cl sig pc frs =
+ "exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
 	(let n		= length ps;
 	     argsoref	= take (n+1) stk;
 	     oref	= last argsoref;