--- a/src/HOL/MicroJava/JVM/Method.thy	Thu Dec 02 09:09:30 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Method.thy	Mon Dec 06 14:23:45 1999 +0100
@@ -40,7 +40,7 @@
 primrec
   "exec_mr Return stk0 frs =
 	(if frs=[] then []
-         else let val = hd stk0; (stk,loc,cn,met,pc) = hd frs
-	      in (val#stk,loc,cn,met,pc)#tl frs)"
+         else let val = hd stk0; (stk,loc,C,sig,pc) = hd frs
+	      in (val#stk,loc,C,sig,pc)#tl frs)"
 
 end