--- a/Nominal/NewParser.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal/NewParser.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -1,5 +1,5 @@
 theory NewParser
-imports "../Nominal-General/Nominal2_Atoms" 
+imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
         "Perm" "NewFv"
@@ -449,9 +449,22 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
-
+atom_decl name
 
-atom_decl name
+nominal_datatype lam =
+  Var name
+| App lam lam
+| Lam x::name t::lam  bind_set x in t
+| Let p::pt t::lam bind_set "bn p" in t
+and pt =
+  P1 name
+| P2 pt pt
+binder
+ bn::"pt \<Rightarrow> atom set" 
+where
+  "bn (P1 x) = {atom x}"
+| "bn (P2 p1 p2) = bn p1 \<union> bn p2"
+
 
 nominal_datatype exp =
   EVar name
@@ -507,10 +520,10 @@
 
 (* some further tests *)
 
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam list"
-| Lam x::"name" t::"lam" bind x in t
+nominal_datatype lam2 =
+  Var2 "name"
+| App2 "lam2" "lam2 list"
+| Lam2 x::"name" t::"lam2" bind x in t
 
 nominal_datatype ty =
   Var "name"