--- a/Nominal/Nominal2.thy	Wed Mar 14 15:41:54 2012 +0000
+++ b/Nominal/Nominal2.thy	Sat Mar 17 05:13:59 2012 +0000
@@ -1,6 +1,10 @@
 theory Nominal2
 imports 
   Nominal2_Base Nominal2_Abs Nominal2_FCB
+keywords
+  "nominal_datatype" :: thy_decl and
+  "nominal_primrec" "nominal_inductive" :: thy_goal and
+  "avoids" "binds"
 uses ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
@@ -710,14 +714,14 @@
 
 val opt_name = Scan.option (P.binding --| Args.colon)
 
-val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
+val anno_typ = S.option (P.name --| @{keyword "::"}) -- P.typ
 
-val bind_mode = P.$$$ "binds" |--
+val bind_mode = @{keyword "binds"} |--
   S.optional (Args.parens 
     (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
 
 val bind_clauses = 
-  P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
+  P.enum "," (bind_mode -- S.repeat1 P.term -- (@{keyword "in"} |-- S.repeat1 P.name) >> triple1)
 
 val cnstr_parser =
   P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2
@@ -725,11 +729,11 @@
 (* datatype parser *)
 val dt_parser =
   (P.type_args_constrained -- P.binding -- P.opt_mixfix >> triple2) -- 
-    (P.$$$ "=" |-- P.enum1 "|" cnstr_parser)
+    (@{keyword "="} |-- P.enum1 "|" cnstr_parser)
 
 (* binding function parser *)
 val bnfun_parser = 
-  S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
+  S.optional (@{keyword "binder"} |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
 
 (* main parser *)
 val main_parser =