# HG changeset patch
# User paulson
# Date 882439990 -3600
# Node ID 75f38104ff8063be64640af6d6938ac36195854f
# Parent  960868c0cbdd3a90f22304a2794feba67c689b7e
UNIV_I no longer counts as safe

diff -r 960868c0cbdd -r 75f38104ff80 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]);