src/HOL/MicroJava/BV/BVSpecTypeSafe.thy

--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Nov 15 18:02:25 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sat Nov 16 22:54:39 2002 +0100
@@ -115,8 +115,8 @@
 qed
 
 lemma match_et_imp_match:
-  "match_exception_table G X pc et = Some handler
-  \<Longrightarrow> match G X pc et = [X]"
+  "match_exception_table G (Xcpt X) pc et = Some handler
+  \<Longrightarrow> match G X pc et = [Xcpt X]"
   apply (simp add: match_some_entry)
   apply (induct et)
   apply (auto split: split_if_asm)