changeset 8038 | a13c3b80d3d4 |
parent 8034 | 6fc37b5c5e98 |
child 8045 | 816f566c414f |
--- a/src/HOL/MicroJava/JVM/Method.thy Mon Nov 29 11:21:50 1999 +0100 +++ b/src/HOL/MicroJava/JVM/Method.thy Mon Nov 29 14:12:53 1999 +0100 @@ -23,7 +23,7 @@ argsoref = take (n+1) stk; oref = last argsoref; xp' = raise_xcpt (oref=Null) NullPointer; - dynT = fst(hp !! (the_Addr oref)); + dynT = fst(the(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)]