--- a/Nominal/Ex/LF.thy	Wed Mar 14 15:41:54 2012 +0000
+++ b/Nominal/Ex/LF.thy	Sat Mar 17 05:13:59 2012 +0000
@@ -147,14 +147,6 @@
 | tex: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> B : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> C : Type; 
          \<Sigma>,(x,C)#\<Gamma> \<turnstile> TApp A (Var x) = TApp B (Var x) : K; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = B : \<Pi>[x:C].K"
 
-thm sig_valid_ctx_valid_trm_valid_ty_valid_kind_valid_trm_equiv_ty_equiv_kind_equiv_def
-thm sig_valid_def
-thm trm_valid_def
-thm ty_valid_def
-thm kind_valid_def
-thm trm_equiv_def
-thm kind_equiv_def
-thm ty_equiv_def
 
 end
 

--- a/Nominal/Ex/Lambda.thy	Wed Mar 14 15:41:54 2012 +0000
+++ b/Nominal/Ex/Lambda.thy	Sat Mar 17 05:13:59 2012 +0000
@@ -887,7 +887,7 @@
 
 text {* tests of functions containing if and case *}
 
-(*consts P :: "lam \<Rightarrow> bool"
+consts P :: "lam \<Rightarrow> bool"
 
 nominal_primrec  
   A :: "lam => lam"
@@ -924,7 +924,7 @@
 apply(perm_simp)
 apply(rule allI)
 apply(rule refl)
-oops*)
+oops
 
 end
 

--- 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 =

--- a/Nominal/Nominal2_Base.thy	Wed Mar 14 15:41:54 2012 +0000
+++ b/Nominal/Nominal2_Base.thy	Sat Mar 17 05:13:59 2012 +0000
@@ -8,6 +8,8 @@
 imports Main 
         "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
+keywords
+  "atom_decl" "equivariance" :: thy_decl 
 uses ("nominal_basics.ML")
      ("nominal_thmdecls.ML")
      ("nominal_permeq.ML")