diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/JVM/Method.thy
--- a/src/HOL/MicroJava/JVM/Method.thy	Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Method.thy	Fri Nov 26 08:46:59 1999 +0100
@@ -23,9 +23,11 @@
 	     argsoref	= take (n+1) stk;
 	     oref	= last argsoref;
 	     xp'	= raise_xcpt (oref=Null) NullPointer;
-	     dynT	= fst(hp \\<And> (the_Addr oref));
-	     (dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps));
-	     frs'	= xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] []
+	     dynT	= fst(hp !! (the_Addr oref));
+	     (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
+	     frs'	= if xp'=None
+	                  then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
+	                  else []
 	 in
 	 (xp' , frs' , drop (n+1) stk , pc+1))"