author | kleing |
Tue, 12 Mar 2002 19:20:23 +0100 | |
changeset 13056 | 4fd18d409fd7 |
parent 13055 | cc37a0778581 |
child 13057 | 805de10ca485 |
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Tue Mar 12 15:18:45 2002 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Tue Mar 12 19:20:23 2002 +0100 @@ -45,7 +45,7 @@ constdefs start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" "start_state G C m \<equiv> - let (C',rT,mxs,mxl,ins,et) = the (method (G,C) (m,[])) in + let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in (None, start_heap G, [([], Null # replicate mxl arbitrary, C, (m,[]), 0)])" end