diff -r cf50eb79d107 -r 29e913950928 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Wed May 30 21:09:11 2007 +0200
+++ b/src/HOL/FixedPoint.thy	Wed May 30 21:09:12 2007 +0200
@@ -241,18 +241,17 @@
   apply simp
   done
 
-lemma Inf_empty_fun_True:
-  "Inf {} = (\<lambda>_. True)"
+lemma Inf_empty_fun:
+  "Inf {} = (\<lambda>_. Inf {})"
   by rule (auto simp add: Inf_fun_def)
 
-lemma Sup_empty_fun_False:
-  "Sup {} = (\<lambda>_. False)"
-proof
-  fix x
-  have aux: "{y\<Colon>bool. \<exists>f\<Colon>'a \<Rightarrow> bool. y = f x} = {True, False}" by auto
-  show "Sup {} x = False"
-  unfolding Sup_def Inf_fun_def by (auto simp add: aux Inf_binary inf_bool_eq)
-qed 
+lemma Sup_empty_fun:
+  "Sup {} = (\<lambda>_. Sup {})"
+proof -
+  have aux: "\<And>x. {y. \<exists>f. y = f x} = UNIV" by auto
+  show ?thesis
+  by (auto simp add: Sup_def Inf_fun_def Inf_binary inf_bool_eq aux)
+qed
 
 
 subsubsection {* Sets *}