diff -r 78b8f9e13300 -r ec054019c910 src/HOL/Real/RealAbs.thy
--- a/src/HOL/Real/RealAbs.thy	Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Real/RealAbs.thy	Fri Nov 02 17:55:24 2001 +0100
@@ -9,6 +9,6 @@
 
 
 defs
-  real_abs_def "abs r == (if (Numeral0::real) <= r then r else -r)"
+  real_abs_def "abs r == (if (0::real) <= r then r else -r)"
 
 end