diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Groups.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -1203,13 +1203,7 @@
 end
 
 class abs =
-  fixes abs :: "'a \<Rightarrow> 'a"
-begin
-
-notation (xsymbols)
-  abs  ("\<bar>_\<bar>")
-
-end
+  fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
 
 class sgn =
   fixes sgn :: "'a \<Rightarrow> 'a"
@@ -1375,7 +1369,7 @@
 lemma dense_eq0_I:
   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
-  apply (cases "abs x=0", simp)
+  apply (cases "\<bar>x\<bar> = 0", simp)
   apply (simp only: zero_less_abs_iff [symmetric])
   apply (drule dense)
   apply (auto simp add: not_less [symmetric])