# HG changeset patch
# User wenzelm
# Date 1191859985 -7200
# Node ID 557a9cd9370cb179a788227b85f9728f341fd68a
# Parent  65830ab42016a1918ac5d464c95b710d4f3d4cfe
turned keywords invariant/freshness_context into reserved indentifiers;

diff -r 65830ab42016 -r 557a9cd9370c src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Mon Oct 08 18:13:04 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Oct 08 18:13:05 2007 +0200
@@ -416,15 +416,17 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["invariant", "freshness_context"];
+val freshness_context = P.reserved "freshness_context";
+val invariant = P.reserved "invariant";
 
-val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME);
-val parser2 =
-  P.$$$ "invariant" |-- P.$$$ ":" |--
-    (Scan.repeat1 P.term >> SOME) -- Scan.optional parser1 NONE ||
+fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- P.$$$ ":") scan;
+
+val parser1 = (freshness_context -- P.$$$ ":") |-- unless_flag P.term >> SOME;
+val parser2 = (invariant -- P.$$$ ":") |--
+    (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
   (parser1 >> pair NONE);
 val parser3 =
-  P.name -- Scan.optional parser2 (NONE, NONE) ||
+  unless_flag P.name -- Scan.optional parser2 (NONE, NONE) ||
   (parser2 >> pair "");
 val parser4 =
   (P.$$$ "unchecked" >> K true) -- Scan.optional parser3 ("", (NONE, NONE)) ||