# HG changeset patch # User wenzelm # Date 1206649268 -3600 # Node ID 758c6fef7b94d0762136bd050d998859ed8c15e0 # Parent ed657432b8b9870d071fe1e4aebfb11a0ebb0e42 avoid ambiguity of State.state vs. JVMType.state; 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 @@ (\e \ set et. fst (snd (snd e)) < length ins)" -- "The method type only contains declared classes:" - check_types :: "jvm_prog \ nat \ nat \ state list \ bool" + check_types :: "jvm_prog \ nat \ nat \ JVMType.state list \ bool" "check_types G mxs mxr phi \ set phi \ states G mxs mxr" -- "An instruction is welltyped if it is applicable and its effect"