diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Wed Apr 14 16:10:44 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Wed Apr 14 16:11:04 2010 +0200
@@ -120,9 +120,6 @@
   Conv.all_conv ctrm 
 end
 
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
-
 (* main conversion *)
 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
 let