diff -r 07f75bf77a33 -r c838477b5c18 src/HOL/Real/RealAbs.thy
--- a/src/HOL/Real/RealAbs.thy	Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/RealAbs.thy	Thu Dec 21 10:16:33 2000 +0100
@@ -9,6 +9,6 @@
 
 
 defs
-  abs_real_def "abs r == (if (#0::real) <= r then r else -r)"
+  real_abs_def "abs r == (if (#0::real) <= r then r else -r)"
 
 end