src/ZF/Tools/typechk.ML

   Theory.setup
    (Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del)
       "declaration of type-checking rule" #>
     Method.setup @{binding typecheck}
       (Method.sections
-        [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}),
-         Args.del -- Args.colon >> K (Method.modifier TC_del @{here})]
+        [Args.add -- Args.colon >> K (Method.modifier TC_add \<^here>),
+         Args.del -- Args.colon >> K (Method.modifier TC_del \<^here>)]
         >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
       "ZF type-checking");
 
 val _ =
   Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"