src/HOL/MicroJava/JVM/Method.thy
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)]