diff -r 29ebbe56f450 -r 428d9cb9a243 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 06:50:49 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 07:11:45 2010 +0800
@@ -31,8 +31,13 @@
 thm trm_raw_assg_raw.size(9 - 16)
 thm eq_iff
 thm eq_iff_simps
+thm bn_defs
+thm fv_eqvt
+thm bn_eqvt
+thm size_eqvt
 
-(* bn / eqvt lemmas for fv / fv_bn / bn *)
+
+(* eqvt lemmas for fv / fv_bn / bn *)
 
 ML {*
   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
@@ -74,8 +79,20 @@
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs}
 *}
 
-thm perm_defs
-thm perm_simps
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms size_eqvt}
+*}
+
+
+
 
 lemma supp_fv:
   "supp t = fv_trm t"