--- a/Nominal/Nominal2.thy	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Nominal2.thy	Thu Mar 13 09:21:31 2014 +0000
@@ -399,8 +399,8 @@
   val qperm_bns = map #qconst qperm_bns_info
 
   val _ = trace_msg (K "Lifting of theorems...")  
-  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
-    prod.cases} 
+  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def
+    prod.case} 
 
   val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, 
          qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, 
@@ -747,6 +747,3 @@
 
 
 end
-
-
-