--- 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))"