--- 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 =