diff -r 493d9c4d7ed5 -r c296c75f4cf4 src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Wed Dec 28 15:08:12 2011 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Wed Dec 28 20:03:13 2011 +0100
@@ -345,7 +345,7 @@
 apply (subgoal_tac [2]
      "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) = 
       ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
-prefer 2 apply simp
+prefer 2 apply blast
 prefer 2 apply blast 
 apply (rule Stable_reachable_EQ_R_AND_nmsg_0
             [simplified Eq_lemma2 Collect_const])