diff -r 6e856be26ac7 -r 947e5f772a9c Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 11 11:41:27 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 11 12:26:24 2010 +0100
@@ -28,7 +28,7 @@
 thm bi_raw.simps
 thm permute_lam_raw_permute_bp_raw.simps
 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars]
-thm fv_lam_raw_fv_bp_raw.simps[no_vars]
+(*thm fv_lam_raw_fv_bp_raw.simps[no_vars]*)
 
 text {* example 2 *}
 
@@ -57,7 +57,7 @@
 
 
 thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars]
-thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
+(*thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]*)
 thm f_raw.simps
 (*thm trm'_pat'_induct
 thm trm'_pat'_perm
@@ -90,8 +90,8 @@
 text {* example type schemes *}
 
 nominal_datatype t =
-  Var "name"
-| Fun "t" "t"
+  VarTS "name"
+| FunTS "t" "t"
 and  tyS =
   All xs::"name set" ty::"t" bind xs in ty