--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Thu Mar 27 19:05:10 2008 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Thu Mar 27 19:22:23 2008 +0100
@@ -10,7 +10,7 @@
constdefs
- exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
+ exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state step_type"
"exec G maxs rT et bs ==
err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"