--- a/src/HOL/MicroJava/BV/Altern.thy Thu Mar 27 19:05:10 2008 +0100
+++ b/src/HOL/MicroJava/BV/Altern.thy Thu Mar 27 19:22:23 2008 +0100
@@ -12,7 +12,7 @@
constdefs
- check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"
+ check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state \<Rightarrow> bool"
"check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,