src/HOL/MicroJava/JVM/JVMExecInstr.thy

 	     xp'	= raise_xcpt (\\<not> cast_ok G C hp oref) ClassCast; 
 	     stk'	= if xp'=None then stk else tl stk
 	 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;
 	     xp'	= raise_xcpt (oref=Null) NullPointer;
 	     dynT	= fst(the(hp(the_Addr oref)));