diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -161,7 +161,7 @@
         where s2:  "s2 = (vT' # oT' # ST', LT')" and
               oT': "G\<turnstile> oT' \<preceq> oT" and
               vT': "G\<turnstile> vT' \<preceq> vT"
-        by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
+        by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp)
       moreover
       from vT' vT
       have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)