src/HOL/UNITY/WFair.ML

--- a/src/HOL/UNITY/WFair.ML	Fri Jun 16 13:39:21 2000 +0200
+++ b/src/HOL/UNITY/WFair.ML	Fri Jun 16 13:41:44 2000 +0200
@@ -41,7 +41,7 @@
 qed "transientE";
 
 Goalw [transient_def] "transient UNIV = {}";
-by Auto_tac;
+by (Blast_tac 1); 
 qed "transient_UNIV";
 
 Goalw [transient_def] "transient {} = UNIV";