| changeset 9550 | 19a6d1289f5e |
| parent 9376 | c32c5696ec2a |
| child 10042 | 7164dc0d24d8 |
--- 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;