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