diff -r 5d06ecfdb472 -r 1135b8de26c3 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy	Mon Dec 28 01:28:28 2015 +0100
@@ -1062,7 +1062,7 @@
   "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
 
 definition
-  "abs (x::'a poly) = (if x < 0 then - x else x)"
+  "\<bar>x::'a poly\<bar> = (if x < 0 then - x else x)"
 
 definition
   "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"