diff -r 21423597a80d -r b8a53e3a0ee2 src/HOL/MicroJava/JVM/JVMExceptions.thy
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -13,12 +13,11 @@
                  start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"
 
 
-consts
-  match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
-                          \<Rightarrow> p_count option"
-primrec
+primrec match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
+    \<Rightarrow> p_count option"
+where
   "match_exception_table G cn pc []     = None"
-  "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
+| "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
                                            then Some (fst (snd (snd e))) 
                                            else match_exception_table G cn pc es)"
 
@@ -27,11 +26,11 @@
   where "ex_table_of m == snd (snd (snd m))"
 
 
-consts
-  find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list \<Rightarrow> jvm_state"
-primrec
+primrec find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list
+    \<Rightarrow> jvm_state"
+where
   "find_handler G xcpt hp [] = (xcpt, hp, [])"
-  "find_handler G xcpt hp (fr#frs) = 
+| "find_handler G xcpt hp (fr#frs) = 
       (case xcpt of
          None \<Rightarrow> (None, hp, fr#frs)
        | Some xc \<Rightarrow>