src/Pure/variable.ML
changeset 21287 a713ae348e8a
parent 20797 c1f0bc7e7d80
child 21355 5c1b1ae737e1
     1.1 --- a/src/Pure/variable.ML	Fri Nov 10 07:44:47 2006 +0100
     1.2 +++ b/src/Pure/variable.ML	Fri Nov 10 10:42:25 2006 +0100
     1.3 @@ -51,8 +51,8 @@
     1.4    val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
     1.5    val import: bool -> thm list -> Proof.context ->
     1.6      ((ctyp list * cterm list) * thm list) * Proof.context
     1.7 -  val tradeT: Proof.context -> (thm list -> thm list) -> thm list -> thm list
     1.8 -  val trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list
     1.9 +  val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    1.10 +  val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    1.11    val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
    1.12    val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
    1.13    val warn_extra_tfrees: Proof.context -> Proof.context -> unit
    1.14 @@ -401,9 +401,9 @@
    1.15  
    1.16  (* import/export *)
    1.17  
    1.18 -fun gen_trade imp exp ctxt f ths =
    1.19 +fun gen_trade imp exp f ctxt ths =
    1.20    let val ((_, ths'), ctxt') = imp ths ctxt
    1.21 -  in exp ctxt' ctxt (f ths') end;
    1.22 +  in exp ctxt' ctxt (f ctxt' ths') end;
    1.23  
    1.24  val tradeT = gen_trade importT exportT;
    1.25  val trade = gen_trade (import true) export;