# HG changeset patch
# User kleing
# Date 1015957223 -3600
# Node ID 4fd18d409fd735611250e5ec2d81c101882bd1a4
# Parent  cc37a0778581215274a788806a58a87b6268d837
workaround for "ins" bug in sml/nj + code generator

diff -r cc37a0778581 -r 4fd18d409fd7 src/HOL/MicroJava/JVM/JVMExec.thy
--- 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