diff -r 0abf74bdf712 -r 3f797ec16f02 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Tue Aug 16 19:25:42 2005 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Aug 17 08:06:12 2005 +0200
@@ -407,7 +407,7 @@
 
 lemma xcpt_app_lemma [code]:
   "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))"
-  by (simp add: list_all_conv)
+  by (simp add: list_all_iff)
 
 lemmas [simp del] = app_def xcpt_app_def