--- a/src/Pure/Isar/code.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Isar/code.ML Wed Dec 06 18:59:33 2017 +0100
@@ -1264,7 +1264,7 @@
structure Codetype_Plugin = Plugin(type T = string);
-val codetype_plugin = Plugin_Name.declare_setup @{binding codetype};
+val codetype_plugin = Plugin_Name.declare_setup \<^binding>\<open>codetype\<close>;
fun type_interpretation f =
Codetype_Plugin.interpretation codetype_plugin
@@ -1539,7 +1539,7 @@
|| Scan.succeed (code_attribute
add_maybe_abs_eqn_liberal);
in
- Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
+ Attrib.setup \<^binding>\<open>code\<close> (Scan.lift code_attribute_parser)
"declare theorems for code generation"
end);