--- a/src/HOL/MicroJava/JVM/JVMExec.thy Tue Dec 05 08:22:49 2000 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Tue Dec 05 14:08:22 2000 +0100
@@ -19,7 +19,7 @@
"exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
(let
- i = snd(snd(snd(the(method (G,C) sig)))) ! pc
+ i = snd(snd(snd(snd(the(method (G,C) sig))))) ! pc
in
Some (exec_instr i G hp stk loc C sig pc frs))"
--- 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 []
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Dec 05 08:22:49 2000 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Dec 05 14:08:22 2000 +0100
@@ -33,6 +33,6 @@
types
bytecode = "instr list"
- jvm_prog = "(nat \<times> bytecode) prog"
+ jvm_prog = "(nat \<times> nat \<times> bytecode) prog"
end