--- a/src/HOL/Real/RealAbs.thy Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Real/RealAbs.thy Fri Oct 05 21:52:39 2001 +0200
@@ -9,6 +9,6 @@
defs
- real_abs_def "abs r == (if (#0::real) <= r then r else -r)"
+ real_abs_def "abs r == (if (Numeral0::real) <= r then r else -r)"
end