src/Pure/ML/ml_thms.ML
changeset 67147 dea94b1aabc3
parent 66067 cdbcb417db67
child 67715 ec46ecb87999
--- a/src/Pure/ML/ml_thms.ML	Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Dec 06 18:59:33 2017 +0100
@@ -40,7 +40,7 @@
 (* attribute source *)
 
 val _ = Theory.setup
-  (ML_Antiquotation.declaration @{binding attributes} Attrib.attribs
+  (ML_Antiquotation.declaration \<^binding>\<open>attributes\<close> Attrib.attribs
     (fn _ => fn srcs => fn ctxt =>
       let val i = serial () in
         ctxt
@@ -69,8 +69,8 @@
   in (decl, ctxt'') end;
 
 val _ = Theory.setup
-  (ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
-   ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
+  (ML_Antiquotation.declaration \<^binding>\<open>thm\<close> (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
+   ML_Antiquotation.declaration \<^binding>\<open>thms\<close> Attrib.thms (K (thm_binding "thms" false)));
 
 
 (* ad-hoc goals *)
@@ -80,7 +80,7 @@
 val goal = Scan.unless (by || and_) Args.embedded_inner_syntax;
 
 val _ = Theory.setup
-  (ML_Antiquotation.declaration @{binding lemma}
+  (ML_Antiquotation.declaration \<^binding>\<open>lemma\<close>
     (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
       (Parse.position by -- Method.parse -- Scan.option Method.parse)))
     (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>