--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Mon Mar 01 13:40:23 2010 +0100
@@ -7,8 +7,7 @@
theory JVMExceptions imports JVMInstructions begin
-constdefs
- match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool"
+definition match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool" where
"match_exception_entry G cn pc ee ==
let (start_pc, end_pc, handler_pc, catch_type) = ee in
start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"