diff -r 296b03b79505 -r 816f566c414f src/HOL/MicroJava/JVM/Method.thy
--- a/src/HOL/MicroJava/JVM/Method.thy	Wed Dec 01 11:20:24 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Method.thy	Wed Dec 01 18:22:28 1999 +0100
@@ -39,8 +39,8 @@
  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)"
+	(if frs=[] then []
+         else let val = hd stk0; (stk,loc,cn,met,pc) = hd frs
+	      in (val#stk,loc,cn,met,pc)#tl frs)"
 
 end