--- a/Nominal/Nominal2.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -514,7 +514,7 @@
   (* lifting of the theorems *)
   val _ = warning "Lifting of Theorems"
   
-  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
     prod.cases} 
 
   val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) =