changeset 10591 | 6d6cb845e841 |
parent 10057 | 8c8d2d0d3ef8 |
child 10897 | 697fab84709e |
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Tue Dec 05 08:22:49 2000 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Tue Dec 05 14:08:22 2000 +0100 @@ -66,7 +66,7 @@ oref = last argsoref; xp' = raise_xcpt (oref=Null) NullPointer; dynT = fst(the(hp(the_Addr oref))); - (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps)); + (dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps)); frs' = if xp'=None then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] else []