diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Groups.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -167,8 +167,8 @@
 
 setup \<open>
   Reorient_Proc.add
-    (fn Const(@{const_name Groups.zero}, _) => true
-      | Const(@{const_name Groups.one}, _) => true
+    (fn Const(\<^const_name>\<open>Groups.zero\<close>, _) => true
+      | Const(\<^const_name>\<open>Groups.one\<close>, _) => true
       | _ => false)
 \<close>
 
@@ -179,10 +179,10 @@
   let
     fun tr' c = (c, fn ctxt => fn T => fn ts =>
       if null ts andalso Printer.type_emphasis ctxt T then
-        Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
+        Syntax.const \<^syntax_const>\<open>_constrain\<close> $ Syntax.const c $
           Syntax_Phases.term_of_typ ctxt T
       else raise Match);
-  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end
+  in map tr' [\<^const_syntax>\<open>Groups.one\<close>, \<^const_syntax>\<open>Groups.zero\<close>] end
 \<close> \<comment> \<open>show types that are presumably too general\<close>
 
 class plus =