src/HOL/HOLCF/Tools/cont_consts.ML

     val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
   in
     [Syntax.Parse_Print_Rule
       (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames),
         fold (fn a => fn t =>
-            Ast.mk_appl (Ast.Constant @{const_syntax Rep_cfun}) [t, Ast.Variable a])
+            Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Rep_cfun\<close>) [t, Ast.Variable a])
           vnames (Ast.Constant name1))] @
     (case mx of
       Infix _ => [extra_parse_rule]
     | Infixl _ => [extra_parse_rule]
     | Infixr _ => [extra_parse_rule]

     ((c, T, NoSyn),
       (Binding.name c2, change_arrow n T, mx),
       trans_rules (syntax c2) (syntax c1) n mx)
   end
 
-fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0
+fun cfun_arity (Type (n, [_, T])) = if n = \<^type_name>\<open>cfun\<close> then 1 + cfun_arity T else 0
   | cfun_arity _ = 0
 
 fun is_contconst (_, _, NoSyn) = false
   | is_contconst (_, _, Binder _) = false    (* FIXME ? *)
   | is_contconst (c, T, mx) =