--- a/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 22:47:45 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 22:48:49 2010 +0200
@@ -1,8 +1,9 @@
 (*  Title:      Nominal2_Eqvt
-    Authors:    Brian Huffman, Christian Urban
+    Author:     Brian Huffman, 
+    Author:     Christian Urban
 
     Equivariance, Supp and Fresh Lemmas for Operators. 
-    (Contains most, but not all such lemmas.)
+    (Contains many, but not all such lemmas.)
 *)
 theory Nominal2_Eqvt
 imports Nominal2_Base Nominal2_Atoms
@@ -10,6 +11,14 @@
      ("nominal_permeq.ML")
 begin
 
+lemma r: "x = x"
+apply(auto)
+done
+
+ML {*
+  prop_of @{thm r}
+*}
+
 section {* Logical Operators *}
 
 lemma eq_eqvt: