--- a/Nominal/Test.thy	Tue Mar 02 16:04:48 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 18:48:20 2010 +0100
@@ -22,8 +22,8 @@
 term Test.BP_raw
 thm bi_raw.simps
 thm permute_lam_raw_permute_bp_raw.simps
-thm alpha_lam_raw_alpha_bp_raw.intros
-thm fv_lam_raw_fv_bp_raw.simps
+thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
+thm fv_lam_raw_fv_bp_raw.simps[no_vars]
 thm eqvts
 
 print_theorems
@@ -135,12 +135,13 @@
 
 (* example 4 from Terms.thy *)
 
-
 nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  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]
 
 (* example 5 from Terms.thy *)
 
@@ -221,7 +222,12 @@
 |  AndL1 n::"name" t::"phd" "name"                              bind n in t
 |  AndL2 n::"name" t::"phd" "name"                              bind n in t
 |  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
-|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in 1, bind c in t
+|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
+
+(* PROBLEM?: why does it create for the Cut AndR ImpL cases
+two permutations, but only one is used *)
+thm alpha_phd_raw.intros[no_vars]
+thm fv_phd_raw.simps[no_vars]
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -336,14 +342,14 @@
 
 (* example 3 from Peter Sewell's bestiary *)
 nominal_datatype exp =
-  Var name
-| App exp exp
-| Lam x::name e::exp bind x in e
-| Let x::name p::pat e1::exp e2::exp bind x in e2, bind "bp p" in e1
+  Var "name"
+| App "exp" "exp"
+| Lam x::"name" e::"exp" bind x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
 and pat =
-  PVar name
+  PVar "name"
 | PUnit
-| PPair pat pat
+| PPair "pat" "pat"
 binder
   bp :: "pat \<Rightarrow> atom set"
 where