src/Tools/coherent.ML

 functor Coherent(Data: COHERENT_DATA) : COHERENT =
 struct
 
 (** misc tools **)
 
-val (trace, trace_setup) = Attrib.config_bool @{binding coherent_trace} (K false);
+val (trace, trace_setup) = Attrib.config_bool \<^binding>\<open>coherent_trace\<close> (K false);
 fun cond_trace ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ();
 
 datatype cl_prf =
   ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
   int list * (term list * cl_prf) list;

       | SOME prf => resolve_tac ctxt'' [thm_of_cl_prf ctxt'' concl [] prf] 1)
     end) ctxt' 1) ctxt;
 
 val _ = Theory.setup
   (trace_setup #>
-   Method.setup @{binding coherent}
+   Method.setup \<^binding>\<open>coherent\<close>
     (Attrib.thms >> (fn rules => fn ctxt =>
         METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
       "prove coherent formula");
 
 end;