src/HOL/MicroJava/BV/Effect.thy

--- a/src/HOL/MicroJava/BV/Effect.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -208,7 +208,8 @@
   "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> 
   \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
   apply (cases i)
-  apply (auto dest!: match_any_match_table match_X_match_table 
+  apply (auto iff: not_None_eq
+	      dest!: match_any_match_table match_X_match_table 
               dest: match_exception_table_in_et)
   done