--- a/Nominal-General/Nominal2_Eqvt.thy	Sun May 02 14:06:26 2010 +0100
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun May 02 16:00:52 2010 +0100
@@ -291,9 +291,7 @@
   by (simp add: fresh_def supp_unit)
 
 
-section {* additional lemmas *}
-
-ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "Pair"} *}
+section {* additional eqvt lemmas *}
 
 lemmas [eqvt] = 
   imp_eqvt [folded induct_implies_def]
@@ -302,7 +300,7 @@
   supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt
 
   (* datatypes *)
-  permute_prod.simps Pair_eqvt permute_list.simps
+  Pair_eqvt permute_list.simps
 
   (* sets *)
   image_eqvt
@@ -311,7 +309,8 @@
 section {* Test cases *}
 
 
-declare [[trace_eqvt = true]]
+declare [[trace_eqvt = false]]
+(* declare [[trace_eqvt = true]] *)
 
 lemma 
   fixes B::"'a::pt"
@@ -391,8 +390,7 @@
 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
 
 
-section {* 
-  Automatic equivariance procedure for inductive definitions *}
+section {* Automatic equivariance procedure for inductive definitions *}
 
 use "nominal_eqvt.ML"