src/HOL/Tools/Meson/meson_tactic.ML

   let val ctxt' = put_claset HOL_cs ctxt
   in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom ctxt' false true 0) ths) end
 
 val _ =
   Theory.setup
-    (Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
+    (Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt =>
       SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
       "MESON resolution proof procedure")
 
 end;