src/HOL/Nominal/nominal_primrec.ML

 (* outer syntax *)
 
 val freshness_context = Parse.reserved "freshness_context";
 val invariant = Parse.reserved "invariant";
 
-fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
-
-val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
-val parser2 = (invariant -- Parse.$$$ ":") |--
+fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- @{keyword ":"}) scan;
+
+val parser1 = (freshness_context -- @{keyword ":"}) |-- unless_flag Parse.term >> SOME;
+val parser2 = (invariant -- @{keyword ":"}) |--
     (Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
   (parser1 >> pair NONE);
 val options =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
+  Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
 
 val _ =
   Outer_Syntax.local_theory_to_proof "nominal_primrec"
     "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
     (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs