diff -r 23c0049e7c40 -r b01057e72233 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Wed Nov 06 14:50:50 2013 +0100
+++ b/src/HOL/Archimedean_Field.thy	Tue Nov 05 21:23:42 2013 +0100
@@ -129,12 +129,8 @@
   fix y z assume
     "of_int y \<le> x \<and> x < of_int (y + 1)"
     "of_int z \<le> x \<and> x < of_int (z + 1)"
-  then have
-    "of_int y \<le> x" "x < of_int (y + 1)"
-    "of_int z \<le> x" "x < of_int (z + 1)"
-    by simp_all
-  from le_less_trans [OF `of_int y \<le> x` `x < of_int (z + 1)`]
-       le_less_trans [OF `of_int z \<le> x` `x < of_int (y + 1)`]
+  with le_less_trans [of "of_int y" "x" "of_int (z + 1)"]
+       le_less_trans [of "of_int z" "x" "of_int (y + 1)"]
   show "y = z" by (simp del: of_int_add)
 qed