src/HOL/Hyperreal/Lim.ML

--- a/src/HOL/Hyperreal/Lim.ML	Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.ML	Mon Oct 08 15:23:20 2001 +0200
@@ -1712,7 +1712,7 @@
 qed "abs_real_of_nat_cancel";
 Addsimps [abs_real_of_nat_cancel];
 
-Goal "~ abs(x) + 1r < x";
+Goal "~ abs(x) + (1::real) < x";
 by (rtac real_leD 1);
 by (auto_tac (claset() addIs [abs_ge_self RS order_trans],simpset()));
 qed "abs_add_one_not_less_self";