--- a/Nominal/Test.thy	Tue Mar 23 07:04:27 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 08:11:11 2010 +0100
@@ -564,37 +564,6 @@
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
-(* example 6 from Terms.thy *)
-
-(* BV is not respectful, needs to fail*)
-(*
-nominal_datatype trm6 =
-  Vr6 "name"
-| Lm6 x::"name" t::"trm6"         bind x in t
-| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
-binder
-  bv6
-where
-  "bv6 (Vr6 n) = {}"
-| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
-*)
-
-(* example 7 from Terms.thy *)
-(* BV is not respectful, needs to fail*)
-(*
-nominal_datatype trm7 =
-  Vr7 "name"
-| Lm7 l::"name" r::"trm7"   bind l in r
-| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
-binder
-  bv7
-where
-  "bv7 (Vr7 n) = {atom n}"
-| "bv7 (Lm7 n t) = bv7 t - {atom n}"
-| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
-*)
-
 (* example 8 from Terms.thy *)
 
 (* Binding in a term under a bn, needs to fail *)
@@ -611,21 +580,6 @@
   "bv8 (Bar0 x) = {}"
 | "bv8 (Bar1 v x b) = {atom v}"
 *)
-(* example 9 from Terms.thy *)
-
-(* BV is not respectful, needs to fail*)
-(*
-nominal_datatype lam9 =
-  Var9 "name"
-| Lam9 n::"name" l::"lam9" bind n in l
-and bla9 =
-  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
-binder
-  bv9
-where
-  "bv9 (Var9 x) = {}"
-| "bv9 (Lam9 x b) = {atom x}"
-*)
 
 (* Type schemes with separate datatypes *)
 nominal_datatype T =