diff -r 315afa77adea -r 6d6cb845e841 src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- 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 []