diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Fields.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -919,8 +919,8 @@
   assume notless: "~ (0 < x)"
   have "~ (1 < inverse x)"
   proof
-    assume "1 < inverse x"
-    also with notless have "... \<le> 0" by simp
+    assume *: "1 < inverse x"
+    also from notless and * have "... \<le> 0" by simp
     also have "... < 1" by (rule zero_less_one) 
     finally show False by auto
   qed