--- a/Nominal/Test.thy	Tue Mar 23 08:45:08 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 08:46:44 2010 +0100
@@ -6,32 +6,6 @@
 
 ML {* val _ = recursive := false  *}
 
-(* example 1 from Terms.thy *)
-
-nominal_datatype trm1 =
-  Vr1 "name"
-| Ap1 "trm1" "trm1"
-| Lm1 x::"name" t::"trm1"       bind x in t
-| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t
-and bp1 =
-  BUnit1
-| BV1 "name"
-| BP1 "bp1" "bp1"
-binder
-  bv1
-where
-  "bv1 (BUnit1) = {}"
-| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
-| "bv1 (BV1 x) = {atom x}"
-
-thm trm1_bp1.fv
-thm trm1_bp1.eq_iff
-thm trm1_bp1.bn
-thm trm1_bp1.perm
-thm trm1_bp1.induct
-thm trm1_bp1.distinct
-thm trm1_bp1.fv[simplified trm1_bp1.supp]
-
 text {* example 3 from Terms.thy *}
 
 nominal_datatype trm3 =