tuned Variable.trade;

--- a/src/FOLP/simp.ML	Fri Nov 10 07:44:47 2006 +0100
+++ b/src/FOLP/simp.ML	Fri Nov 10 10:42:25 2006 +0100
@@ -222,8 +222,8 @@
 
 fun normed_rews congs =
   let val add_norms = add_norm_tags congs in
-    fn thm => Variable.tradeT (Variable.thm_context thm)
-      (map (add_norms o mk_trans) o maps mk_rew_rules) [thm]
+    fn thm => Variable.tradeT
+      (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm]
   end;
 
 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];

--- a/src/HOL/Library/EfficientNat.thy	Fri Nov 10 07:44:47 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Fri Nov 10 10:42:25 2006 +0100
@@ -248,9 +248,9 @@
                  SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
                Suc_if_eq')) (Thm.forall_intr cv' th)
       in
-        case List.mapPartial (fn th'' =>
+        case map_filter (fn th'' =>
             SOME (th'', singleton
-              (Variable.trade (Variable.thm_context th'') (fn [th'''] => [th''' RS th'])) th'')
+              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
           handle THM _ => NONE) thms of
             [] => NONE
           | thps =>
@@ -309,7 +309,7 @@
   in
     if forall (can (dest o concl_of)) ths andalso
       exists (fn th => member (op =) (foldr add_term_consts
-        [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) "Suc") ths
+        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
     then remove_suc_clause thy ths else ths
   end;
 

--- a/src/Pure/variable.ML	Fri Nov 10 07:44:47 2006 +0100
+++ b/src/Pure/variable.ML	Fri Nov 10 10:42:25 2006 +0100
@@ -51,8 +51,8 @@
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import: bool -> thm list -> Proof.context ->
     ((ctyp list * cterm list) * thm list) * Proof.context
-  val tradeT: Proof.context -> (thm list -> thm list) -> thm list -> thm list
-  val trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list
+  val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
+  val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
   val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
   val warn_extra_tfrees: Proof.context -> Proof.context -> unit
@@ -401,9 +401,9 @@
 
 (* import/export *)
 
-fun gen_trade imp exp ctxt f ths =
+fun gen_trade imp exp f ctxt ths =
   let val ((_, ths'), ctxt') = imp ths ctxt
-  in exp ctxt' ctxt (f ths') end;
+  in exp ctxt' ctxt (f ctxt' ths') end;
 
 val tradeT = gen_trade importT exportT;
 val trade = gen_trade (import true) export;