diff -r ed657432b8b9 -r 758c6fef7b94 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Mar 27 19:49:24 2008 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Mar 27 21:21:08 2008 +0100
@@ -23,7 +23,7 @@
                      (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
 
   -- "The method type only contains declared classes:"
-  check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
+  check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool"
   "check_types G mxs mxr phi \<equiv> set phi \<subseteq> states G mxs mxr"
 
   -- "An instruction is welltyped if it is applicable and its effect"