src/HOL/MicroJava/JVM/Method.thy
changeset 8038 a13c3b80d3d4
parent 8034 6fc37b5c5e98
child 8045 816f566c414f
equal deleted inserted replaced
8037:18f10850aca5 8038:a13c3b80d3d4
    21  "exec_mi (Invoke mn ps) G hp stk pc =
    21  "exec_mi (Invoke mn ps) G hp stk pc =
    22 	(let n		= length ps;
    22 	(let n		= length ps;
    23 	     argsoref	= take (n+1) stk;
    23 	     argsoref	= take (n+1) stk;
    24 	     oref	= last argsoref;
    24 	     oref	= last argsoref;
    25 	     xp'	= raise_xcpt (oref=Null) NullPointer;
    25 	     xp'	= raise_xcpt (oref=Null) NullPointer;
    26 	     dynT	= fst(hp !! (the_Addr oref));
    26 	     dynT	= fst(the(hp(the_Addr oref)));
    27 	     (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
    27 	     (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
    28 	     frs'	= if xp'=None
    28 	     frs'	= if xp'=None
    29 	                  then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
    29 	                  then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
    30 	                  else []
    30 	                  else []
    31 	 in
    31 	 in