diff -r 2d811ae6752a -r c68717c16013 src/HOL/HoareParallel/Gar_Coll.thy
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Wed Dec 06 01:12:36 2006 +0100
@@ -798,7 +798,7 @@
 apply simp_all
 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 ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
 done
 
 subsubsection {* Interference freedom Mutator-Collector *}