src/Pure/Isar/code.ML
changeset 67147 dea94b1aabc3
parent 67032 ed499d1252fc
child 67522 9e712280cc37
--- 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);