diff -r 283107142592 -r 158b924b5153 src/HOL/MicroJava/BV/Altern.thy
--- 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,