--- a/Nominal/NewParser.thy	Tue Apr 27 22:45:50 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Apr 27 23:11:40 2010 +0200
@@ -504,6 +504,20 @@
 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
 
 
+(* some further tests *)
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam list"
+| Lam x::"name" t::"lam" bind x in t
+
+nominal_datatype ty =
+  Var "name"
+| Fun "ty" "ty"
+
+nominal_datatype tys =
+  All xs::"name fset" ty::"ty_raw" bind xs in ty
+
 
 
 end