diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Rat.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -451,7 +451,7 @@
   "x \<le> (y::rat) \<longleftrightarrow> x < y \<or> x = y"
 
 definition
-  "abs (a::rat) = (if a < 0 then - a else a)"
+  "\<bar>a::rat\<bar> = (if a < 0 then - a else a)"
 
 definition
   "sgn (a::rat) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"