src/HOL/Set.ML

--- a/src/HOL/Set.ML	Wed Dec 17 18:13:43 1997 +0100
+++ b/src/HOL/Set.ML	Thu Dec 18 11:13:10 1997 +0100
@@ -216,7 +216,8 @@
 qed_goalw "UNIV_I" Set.thy [UNIV_def] "x : UNIV"
   (fn _ => [rtac CollectI 1, rtac TrueI 1]);
 
-AddIffs [UNIV_I];
+Addsimps [UNIV_I];
+AddIs    [UNIV_I];  (*unsafe makes it less likely to cause problems*)
 
 qed_goal "subset_UNIV" Set.thy "A <= UNIV"
   (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);