diff -r aa5059a00f41 -r 6fd3fc3254ee Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Wed Sep 21 17:16:11 2011 +0900
+++ b/Nominal/Ex/TypeVarsTest.thy	Wed Sep 21 10:23:06 2011 +0200
@@ -44,6 +44,15 @@
 | Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
 
 
+nominal_datatype 'a foo = 
+  Node x::"name" f::"'a foo" binds x in f
+| Leaf "'a"
+
+term "Leaf"
+
+
+
+
 end