diff -r 08e4d3cbcf8c -r 894930834ca8 Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Sun Apr 11 22:47:45 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Sun Apr 11 22:48:49 2010 +0200
@@ -71,7 +71,6 @@
   Conv.no_conv ctrm
 end
 
-
 (* conversion for applications: 
    only applies the conversion, if the head of the
    application is not a "bad head" *)
@@ -132,8 +131,8 @@
     then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
     else Conv.first_conv
 
-  val pre_thms = (map safe_mk_equiv user_thms) @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt)
-  val post_thms = @{thms permute_pure[THEN eq_reflection]}
+  val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
+  val post_thms = map safe_mk_equiv @{thms permute_pure}
 in
   first_conv_wrapper
     [ More_Conv.rewrs_conv pre_thms,