--- /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
+
+

--- a/Nominal/Ex/Test.thy	Tue May 04 14:13:18 2010 +0200
+++ b/Nominal/Ex/Test.thy	Tue May 04 14:21:18 2010 +0200
@@ -20,23 +20,6 @@
 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 *)
 
-(* example 8 from Terms.thy *)
-
-(* Binding in a term under a bn, needs to fail *)
-(*
-nominal_datatype foo8 =
-  Foo0 "name"
-| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
-and bar8 =
-  Bar0 "name"
-| Bar1 "name" s::"name" b::"bar8" bind s in b
-binder
-  bv8
-where
-  "bv8 (Bar0 x) = {}"
-| "bv8 (Bar1 v x b) = {atom v}"
-*)
-
 end
 
 

--- a/TODO	Tue May 04 14:13:18 2010 +0200
+++ b/TODO	Tue May 04 14:21:18 2010 +0200
@@ -14,6 +14,7 @@
 - types of bindings match types of binding functions
 - fsets are not bound in lst bindings
 - bound arguments are not datatypes
+- binder is referred to by name and not by type
 
 Smaller things: