--- a/Nominal-General/nominal_permeq.ML	Wed Apr 14 14:41:54 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Wed Apr 14 15:02:07 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