diff -r 80dabcaafc38 -r b395b902cf0d Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 02 15:10:47 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 15:11:41 2010 +0100
@@ -24,7 +24,7 @@
 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 eqvts
 
 print_theorems
 
@@ -332,8 +332,6 @@
  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
 *)
 
-thm bv_raw.simps
-
 end