src/HOL/HOLCF/IOA/meta_theory/Sequence.thy

--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -836,7 +836,7 @@
   ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)"
 apply (drule divide_Seq2)
 (*Auto_tac no longer proves it*)
-apply fastsimp
+apply fastforce
 done
 
 lemmas [simp] = FilterPQ FilterConc Conc_cong