--- a/Nominal-General/nominal_permeq.ML	Mon May 17 17:34:02 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Mon May 17 20:23:40 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 *)

--- a/Nominal/Manual/Term4.thy	Mon May 17 17:34:02 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Mon May 17 20:23:40 2010 +0100
@@ -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))"