--- a/Nominal/Ex/Test.thy	Tue May 11 12:18:26 2010 +0100
+++ b/Nominal/Ex/Test.thy	Tue May 11 14:58:46 2010 +0100
@@ -10,12 +10,16 @@
 (* example 4 from Terms.thy *)
 (* fv_eqvt does not work, we need to repaire defined permute functions
    defined fv and defined alpha... *)
-(* lists-datastructure does not work yet
-nominal_datatype trm4 =
-  Vr4 "name"
-| Ap4 "trm4" "trm4 list"
-| Lm4 x::"name" t::"trm4"  bind x in t
+(* lists-datastructure does not work yet *)
 
+(*
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm list"
+| Lm x::"name" t::"trm"  bind x in t
+*)
+
+(*
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 *)