--- a/Nominal/Parser.thy	Fri Apr 23 11:12:38 2010 +0200
+++ b/Nominal/Parser.thy	Sat Apr 24 09:49:23 2010 +0200
@@ -625,9 +625,14 @@
     map_index (prep_typ binds) annos
   end
 
+  val result = map (map (map (map (fn (a, b, c) => 
+    (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type)))))
+      (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
+ 
+  val _ = warning (@{make_string} result)
+
 in
-  map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type)))))
-  (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
+  result
 end
 *}
 
@@ -660,6 +665,51 @@
 end
 *}
 
+atom_decl name
+
+nominal_datatype exp =
+  EVar name
+| EUnit
+| EPair exp exp
+| ELetRec l::lrbs e::exp     bind "b_lrbs l" in e
+
+and fnclause =
+  K x::name p::pat f::exp    bind "b_pat p" in f 
+
+and fnclauses =
+  S fnclause
+| ORs fnclause fnclauses
+
+and lrb =
+  Clause fnclauses
+
+and lrbs =
+  Single lrb
+| More lrb lrbs
+
+and pat =
+  PVar name
+| PUnit
+| PPair pat pat
+
+binder
+  b_lrbs      :: "lrbs \<Rightarrow> atom set" and
+  b_pat       :: "pat \<Rightarrow> atom set" and
+  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
+  b_fnclause  :: "fnclause \<Rightarrow> atom set" and
+  b_lrb       :: "lrb \<Rightarrow> atom set"
+
+where
+  "b_lrbs (Single l) = b_lrb l"
+| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
+| "b_pat (PVar x) = {atom x}"
+| "b_pat (PUnit) = {}"
+| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
+| "b_fnclauses (S fc) = (b_fnclause fc)"
+| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
+| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K x pat exp) = {atom x}"
+
 
 end