diff -r 95aac598a526 -r 6297629f024c Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Mon May 17 17:54:07 2010 +0100
+++ b/Nominal-General/nominal_permeq.ML	Mon May 17 18:13:39 2010 +0100
@@ -127,10 +127,10 @@
   val post_thms = map safe_mk_equiv @{thms permute_pure}
 in
   first_conv_wrapper
-    [ More_Conv.rewrs_conv pre_thms,
+    [ Conv.rewrs_conv pre_thms,
       eqvt_apply_conv,
       eqvt_lambda_conv,
-      More_Conv.rewrs_conv post_thms,
+      Conv.rewrs_conv post_thms,
       progress_info_conv ctxt strict_flag excluded
     ] ctrm
 end
@@ -141,12 +141,12 @@
 
 (* raises an error if some permutations cannot be eliminated *)
 fun eqvt_strict_tac ctxt user_thms excluded = 
-  CONVERSION (More_Conv.top_conv 
+  CONVERSION (Conv.top_conv 
     (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt)
 
 (* prints a warning message if some permutations cannot be eliminated *)
 fun eqvt_tac ctxt user_thms excluded = 
-  CONVERSION (More_Conv.top_conv 
+  CONVERSION (Conv.top_conv 
     (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt)
 
 (* setup of the configuration value *)