diff -r 4bed56dc95fb -r a7fba340058c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Dec 08 13:34:50 2010 +0100
+++ b/src/HOL/Set.thy	Wed Dec 08 13:34:51 2010 +0100
@@ -540,7 +540,7 @@
 
 lemma UNIV_def:
   "UNIV = {x. True}"
-  by (simp add: top_fun_eq top_bool_eq Collect_def)
+  by (simp add: top_fun_def top_bool_def Collect_def)
 
 lemma UNIV_I [simp]: "x : UNIV"
   by (simp add: UNIV_def)
@@ -573,7 +573,7 @@
 
 lemma empty_def:
   "{} = {x. False}"
-  by (simp add: bot_fun_eq bot_bool_eq Collect_def)
+  by (simp add: bot_fun_def bot_bool_def Collect_def)
 
 lemma empty_iff [simp]: "(c : {}) = False"
   by (simp add: empty_def)
@@ -625,6 +625,7 @@
 lemma Pow_not_empty: "Pow A \<noteq> {}"
   using Pow_top by blast
 
+
 subsubsection {* Set complement *}
 
 lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
@@ -649,7 +650,7 @@
 subsubsection {* Binary union -- Un *}
 
 abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
-  "op Un \<equiv> sup"
+  "union \<equiv> sup"
 
 notation (xsymbols)
   union  (infixl "\<union>" 65)
@@ -659,7 +660,7 @@
 
 lemma Un_def:
   "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
-  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
+  by (simp add: sup_fun_def sup_bool_def Collect_def mem_def)
 
 lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   by (unfold Un_def) blast
@@ -701,7 +702,7 @@
 
 lemma Int_def:
   "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
-  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
+  by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
 
 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   by (unfold Int_def) blast