diff -r 827cac8abecc -r 026e7c6a6d08 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Tue Sep 22 15:36:55 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/BV/Effect.thy
-    ID:         $Id$
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
 *)
@@ -391,7 +390,7 @@
   with Pair 
   have "?app s \<Longrightarrow> ?P s" by (simp only:)
   moreover
-  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
+  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
   ultimately
   show ?thesis by (rule iffI) 
 qed