# HG changeset patch
# User paulson
# Date 961155704 -7200
# Node ID 090d450af656d73cd8a4004b8efce1fcb9fc30bb
# Parent  b36787a56a1f795ce4a128a1444ba58c33a9edaa
fixed for removal of subset_empty

diff -r b36787a56a1f -r 090d450af656 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";