--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Mon Sep 12 07:55:43 2011 +0200
@@ -299,7 +299,7 @@
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
(* a~: act B; a~: act A *)
-apply (fastsimp intro!: ext_is_act simp: externals_of_par)
+apply (fastforce intro!: ext_is_act simp: externals_of_par)
done
declare FiniteConc [simp]
@@ -452,7 +452,7 @@
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
(* Case a~:A, a~:B *)
-apply (fastsimp intro!: ext_is_act simp: externals_of_par)
+apply (fastforce intro!: ext_is_act simp: externals_of_par)
done