--- a/src/ZF/UNITY/UNITY.ML	Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/UNITY.ML	Fri Jun 20 12:10:45 2003 +0200
@@ -511,9 +511,9 @@
 
 Goalw [constrains_def, st_set_def] 
   "[| F:A co A' |] ==> A <= A'";
-by Auto_tac;
-by (Blast_tac 1);
+by (Force_tac 1); 
 qed "constrains_imp_subset";
+
 (*The reasoning is by subsets since "co" refers to single actions
   only.  So this rule isn't that useful.*)