# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274175979 -7200
# Node ID 3c4eff4a73daf94d591c802e87861f6aa1ff7c92
# Parent  d7d4491535a9c74e1cde6846993404fac92525fc# Parent  ad608532c7cd2b48fbbfb32051c8244e66c5edd7
merge

diff -r d7d4491535a9 -r 3c4eff4a73da Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Tue May 18 11:45:49 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Tue May 18 11:46:19 2010 +0200
@@ -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 *)
diff -r d7d4491535a9 -r 3c4eff4a73da Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Tue May 18 11:45:49 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Tue May 18 11:46:19 2010 +0200
@@ -27,7 +27,7 @@
 
 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *}
 
-local_setup {* fn ctxt => let val (_, _, ctxt') = define_raw_fv descr sorts [] bl ctxt in ctxt' end *}
+local_setup {* fn ctxt => let val (_, _, _, ctxt') = define_raw_fvs descr sorts [] bl ctxt in ctxt' end *}
 lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*)
 
 lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"