--- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Thu Nov 25 12:01:28 1999 +0100
@@ -14,7 +14,7 @@
| MO manipulate_object
| CH check_object
| MI meth_inv
- | MR
+ | MR meth_ret
| OS op_stack
| BR branch
@@ -51,7 +51,7 @@
in
(xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
- | MR \\<Rightarrow> (let frs' = exec_mr stk frs in
+ | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
(None,hp,frs'))
| OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc