--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Term8.thy	Tue May 04 14:21:18 2010 +0200
@@ -0,0 +1,23 @@
+theory Term8
+imports "../NewParser"
+begin
+
+(* example 8 from Terms.thy *)
+
+atom_decl name
+
+nominal_datatype foo =
+  Foo0 "name"
+| Foo1 b::"bar" f::"foo" bind_set "bv b" in f
+and bar =
+  Bar0 "name"
+| Bar1 "name" s::"name" b::"bar" bind_set s in b
+binder
+  bv
+where
+  "bv (Bar0 x) = {}"
+| "bv (Bar1 v x b) = {atom v}"
+
+end
+
+