--- a/Nominal/Ex/TypeVarsTest.thy	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Jul 09 02:32:46 2015 +0100
@@ -2,6 +2,37 @@
 imports "../Nominal2" 
 begin
 
+atom_decl var
+
+ML {* trace := true *}
+declare [[ML_print_depth = 1000]]
+
+nominal_datatype exp =
+          Var var
+        | App exp var
+        | LetA as::assn body::exp binds "bn as" in "body" "as"
+        | Lam x::var body::exp binds x in body
+        and assn =
+          ANil | ACons var exp assn
+        binder
+          bn
+        where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"
+
+nominal_datatype ('ann::fs) exp2 =
+  Var var
+| App "'ann exp2" var
+| LetA as::"'ann assn2" body::"'ann exp2" binds "bnn as" in body as
+| Lam x::var body::"'ann exp2" binds x in body
+and ('ann::fs) assn2 =
+  ANil 
+| ACons var "'ann exp2" 'ann "'ann assn2"
+binder
+  bnn :: "('ann::fs) assn2 \<Rightarrow> atom list"
+where 
+  "bnn ANil = []" 
+| "bnn (ACons x a t as) = (atom x) # (bnn as)"
+
+
 (* a nominal datatype with type variables and sorts *)
 
 
@@ -54,7 +85,6 @@
 
 
 
-
 end