src/HOL/UNITY/Constrains.thy

--- a/src/HOL/UNITY/Constrains.thy	Sat Sep 10 20:41:27 2011 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Sat Sep 10 21:47:55 2011 +0200
@@ -181,7 +181,9 @@
 
 lemma Constrains_cancel:
      "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
-by (simp add: Constrains_eq_constrains constrains_def, blast)
+apply (simp add: Constrains_eq_constrains constrains_def)
+apply best
+done
 
 
 subsection{*Stable*}