src/HOL/Real/RealAbs.ML

--- a/src/HOL/Real/RealAbs.ML	Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RealAbs.ML	Tue Jan 16 12:20:52 2001 +0100
@@ -213,7 +213,7 @@
 qed "real_0_less_abs_iff";
 Addsimps [real_0_less_abs_iff];
 
-Goal "abs (real_of_nat x) = real_of_nat x";
+Goal "abs (real x) = real (x::nat)";
 by (auto_tac (claset() addIs [abs_eqI1],
               simpset() addsimps [rename_numerals real_of_nat_ge_zero]));
 qed "abs_real_of_nat_cancel";