--- a/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 22:48:49 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Mon Apr 12 13:34:54 2010 +0200
@@ -11,13 +11,6 @@
      ("nominal_permeq.ML")
 begin
 
-lemma r: "x = x"
-apply(auto)
-done
-
-ML {*
-  prop_of @{thm r}
-*}
 
 section {* Logical Operators *}
 
@@ -266,10 +259,7 @@
   atom_eqvt add_perm_eqvt
 
 lemmas [eqvt_raw] =
-  permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) 
-
-thm eqvts
-thm eqvts_raw
+  permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *)
 
 text {* helper lemmas for the eqvt_tac *}