1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 15 19:48:19 2012 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 15 20:07:00 2012 +0100
     1.3 @@ -392,14 +392,14 @@
     1.4  val freshness_context = Parse.reserved "freshness_context";
     1.5  val invariant = Parse.reserved "invariant";
     1.6  
     1.7 -fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
     1.8 +fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- @{keyword ":"}) scan;
     1.9  
    1.10 -val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
    1.11 -val parser2 = (invariant -- Parse.$$$ ":") |--
    1.12 +val parser1 = (freshness_context -- @{keyword ":"}) |-- unless_flag Parse.term >> SOME;
    1.13 +val parser2 = (invariant -- @{keyword ":"}) |--
    1.14      (Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
    1.15    (parser1 >> pair NONE);
    1.16  val options =
    1.17 -  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
    1.18 +  Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
    1.19  
    1.20  val _ =
    1.21    Outer_Syntax.local_theory_to_proof "nominal_primrec"