tuned Variable.trade;
authorwenzelm
Fri Nov 10 10:42:25 2006 +0100 (2006-11-10)
changeset 21287a713ae348e8a
parent 21286 b5e7b80caa6a
child 21288 2c7d3d120418
tuned Variable.trade;
src/FOLP/simp.ML
src/HOL/Library/EfficientNat.thy
src/Pure/variable.ML
     1.1 --- a/src/FOLP/simp.ML	Fri Nov 10 07:44:47 2006 +0100
     1.2 +++ b/src/FOLP/simp.ML	Fri Nov 10 10:42:25 2006 +0100
     1.3 @@ -222,8 +222,8 @@
     1.4  
     1.5  fun normed_rews congs =
     1.6    let val add_norms = add_norm_tags congs in
     1.7 -    fn thm => Variable.tradeT (Variable.thm_context thm)
     1.8 -      (map (add_norms o mk_trans) o maps mk_rew_rules) [thm]
     1.9 +    fn thm => Variable.tradeT
    1.10 +      (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm]
    1.11    end;
    1.12  
    1.13  fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
     2.1 --- a/src/HOL/Library/EfficientNat.thy	Fri Nov 10 07:44:47 2006 +0100
     2.2 +++ b/src/HOL/Library/EfficientNat.thy	Fri Nov 10 10:42:25 2006 +0100
     2.3 @@ -248,9 +248,9 @@
     2.4                   SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
     2.5                 Suc_if_eq')) (Thm.forall_intr cv' th)
     2.6        in
     2.7 -        case List.mapPartial (fn th'' =>
     2.8 +        case map_filter (fn th'' =>
     2.9              SOME (th'', singleton
    2.10 -              (Variable.trade (Variable.thm_context th'') (fn [th'''] => [th''' RS th'])) th'')
    2.11 +              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
    2.12            handle THM _ => NONE) thms of
    2.13              [] => NONE
    2.14            | thps =>
    2.15 @@ -309,7 +309,7 @@
    2.16    in
    2.17      if forall (can (dest o concl_of)) ths andalso
    2.18        exists (fn th => member (op =) (foldr add_term_consts
    2.19 -        [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) "Suc") ths
    2.20 +        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
    2.21      then remove_suc_clause thy ths else ths
    2.22    end;
    2.23  
     3.1 --- a/src/Pure/variable.ML	Fri Nov 10 07:44:47 2006 +0100
     3.2 +++ b/src/Pure/variable.ML	Fri Nov 10 10:42:25 2006 +0100
     3.3 @@ -51,8 +51,8 @@
     3.4    val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
     3.5    val import: bool -> thm list -> Proof.context ->
     3.6      ((ctyp list * cterm list) * thm list) * Proof.context
     3.7 -  val tradeT: Proof.context -> (thm list -> thm list) -> thm list -> thm list
     3.8 -  val trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list
     3.9 +  val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    3.10 +  val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    3.11    val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
    3.12    val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
    3.13    val warn_extra_tfrees: Proof.context -> Proof.context -> unit
    3.14 @@ -401,9 +401,9 @@
    3.15  
    3.16  (* import/export *)
    3.17  
    3.18 -fun gen_trade imp exp ctxt f ths =
    3.19 +fun gen_trade imp exp f ctxt ths =
    3.20    let val ((_, ths'), ctxt') = imp ths ctxt
    3.21 -  in exp ctxt' ctxt (f ths') end;
    3.22 +  in exp ctxt' ctxt (f ctxt' ths') end;
    3.23  
    3.24  val tradeT = gen_trade importT exportT;
    3.25  val trade = gen_trade (import true) export;