# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274116419 -3600
# Node ID 6297629f024cfd0ca15d362e259c2177dc1ac09c
# Parent  95aac598a5269f309b8b0283edd5bbf47e5c4aa5
updated to new Isabelle (More_Conv -> Conv)

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 *)