diff -r faf62905cd53 -r ad878aff9c15 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Fri Mar 02 09:35:32 2012 +0100
+++ b/src/HOL/SupInf.thy	Fri Mar 02 09:35:33 2012 +0100
@@ -445,11 +445,9 @@
   fixes x :: real
   shows "max x y = Sup {x,y}"
 proof-
-  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
-  from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
+  have "Sup {x,y} \<le> max x y" by (simp add: Sup_finite_le_iff)
   moreover
-  have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
-    by (simp add: linorder_linear)
+  have "max x y \<le> Sup {x,y}" by (simp add: linorder_linear Sup_finite_ge_iff)
   ultimately show ?thesis by arith
 qed
 
@@ -457,12 +455,9 @@
   fixes x :: real
   shows "min x y = Inf {x,y}"
 proof-
-  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
-  from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
-    by (simp add: linorder_linear)
+  have "Inf {x,y} \<le> min x y" by (simp add: linorder_linear Inf_finite_le_iff)
   moreover
-  have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
-    by simp
+  have "min x y \<le> Inf {x,y}" by (simp add:  Inf_finite_ge_iff)
   ultimately show ?thesis by arith
 qed