src/Doc/more_antiquote.ML

 struct
 
 (* class specifications *)
 
 val _ =
-  Theory.setup (Thy_Output.antiquotation_pretty @{binding class_spec} (Scan.lift Args.name)
+  Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\<open>class_spec\<close> (Scan.lift Args.name)
     (fn ctxt => fn s =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val class = Sign.intern_class thy s;
       in Pretty.chunks (Class.pretty_specification thy class) end));

     val ctxt' = Variable.set_body false ctxt;
     val ((_, [thm]), _) = Variable.import true [thm] ctxt';
   in thm end;
 
 val _ =
-  Theory.setup (Thy_Output.antiquotation_pretty @{binding code_thms} Args.term
+  Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\<open>code_thms\<close> Args.term
     (fn ctxt => fn raw_const =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val const = Code.check_const thy raw_const;
         val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };