diff -r 340df9f3491f -r 22f665a2e91c src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -102,7 +102,7 @@
         by clarify (rule pp_ub1)
       with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp
       with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1"
-        by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r)
+        by (fastforce dest!: mapD lesub_step_typeD intro: trans_r)
       moreover 
       from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2)
       with sum have "x <=_r ?s1" by simp