--- a/Nominal/Test.thy	Tue Mar 02 17:11:58 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 17:48:41 2010 +0100
@@ -4,6 +4,8 @@
 
 text {* example 1 *}
 
+(* ML {* set show_hyps *} *)
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -77,11 +79,13 @@
   All xs::"name list" ty::"t_raw" bind xs in ty
 *)
 
+
+(* alpha_eqvt fails...
 nominal_datatype t = 
   Var "name" 
 | Fun "t" "t"
 and  tyS = 
-  All xs::"name set" ty::"t" bind xs in ty
+  All xs::"name set" ty::"t" bind xs in ty *)
 
 (* example 1 from Terms.thy *)
 
@@ -135,12 +139,12 @@
 
 (* example 4 from Terms.thy *)
 
-
+(* fv_eqvt does not work, we need to repaire defined permute functions...
 nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  bind x in t
-
+*)
 
 (* example 5 from Terms.thy *)