diff -r f48c4a3a34bc -r a2fb9d553aad src/HOL/HoareParallel/Gar_Coll.thy
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Sat Jul 08 12:54:37 2006 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Sat Jul 08 12:54:38 2006 +0200
@@ -796,9 +796,9 @@
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
 apply(tactic {* TRYALL (etac disjE) *})
 apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),Force_tac, assume_tac]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),Force_tac]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),Force_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
 done
 
 subsubsection {* Interference freedom Mutator-Collector *}