diff -r 826c6222cca2 -r 1eaae1a2f8ff src/HOL/MicroJava/JVM/Method.thy
--- a/src/HOL/MicroJava/JVM/Method.thy	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Method.thy	Thu Nov 25 12:01:28 1999 +0100
@@ -12,13 +12,13 @@
 
 datatype 
  meth_inv = 
-   Invokevirtual   mname (ty list)      (** inv. instance meth of an object **)
+   Invoke mname (ty list)      (** inv. instance meth of an object **)
  
 consts
  exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count] 
 		\\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)" 
 primrec
- "exec_mi (Invokevirtual mn ps) G hp stk pc =
+ "exec_mi (Invoke mn ps) G hp stk pc =
 	(let n		= length ps;
 	     argsoref	= take (n+1) stk;
 	     oref	= last argsoref;
@@ -30,11 +30,14 @@
 	 (xp' , frs' , drop (n+1) stk , pc+1))"
 
 
-constdefs
- exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
-"exec_mr stk0 frs \\<equiv>
-	 (let val			= hd stk0;
-	      (stk,loc,cn,met,pc) = hd frs
+datatype 
+ meth_ret = Return
+ 
+consts
+ exec_mr :: "[meth_ret,opstack,frame list] \\<Rightarrow> frame list"
+primrec
+  "exec_mr Return stk0 frs =
+	 (let val = hd stk0; (stk,loc,cn,met,pc) = hd frs
 	  in
 	  (val#stk,loc,cn,met,pc)#tl frs)"