workaround for "ins" bug in sml/nj + code generator
authorkleing
Tue Mar 12 19:20:23 2002 +0100 (2002-03-12)
changeset 130564fd18d409fd7
parent 13055 cc37a0778581
child 13057 805de10ca485
workaround for "ins" bug in sml/nj + code generator
src/HOL/MicroJava/JVM/JVMExec.thy
     1.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Mar 12 15:18:45 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Mar 12 19:20:23 2002 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  constdefs  
     1.5    start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state"
     1.6    "start_state G C m \<equiv>
     1.7 -  let (C',rT,mxs,mxl,ins,et) = the (method (G,C) (m,[])) in
     1.8 +  let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in
     1.9      (None, start_heap G, [([], Null # replicate mxl arbitrary, C, (m,[]), 0)])"
    1.10  
    1.11  end