1.1 --- a/src/Pure/variable.ML	Wed Jun 24 20:52:49 2009 +0200
     1.2 +++ b/src/Pure/variable.ML	Wed Jun 24 21:28:02 2009 +0200
     1.3 @@ -51,9 +51,9 @@
     1.4      (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
     1.5    val importT_terms: term list -> Proof.context -> term list * Proof.context
     1.6    val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
     1.7 -  val importT_thms: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
     1.8 +  val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
     1.9    val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
    1.10 -  val import_thms: bool -> thm list -> Proof.context ->
    1.11 +  val import: bool -> thm list -> Proof.context ->
    1.12      ((ctyp list * cterm list) * thm list) * Proof.context
    1.13    val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    1.14    val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    1.15 @@ -424,7 +424,7 @@
    1.16    let val (inst, ctxt') = import_inst is_open ts ctxt
    1.17    in (map (TermSubst.instantiate inst) ts, ctxt') end;
    1.18  
    1.19 -fun importT_thms ths ctxt =
    1.20 +fun importT ths ctxt =
    1.21    let
    1.22      val thy = ProofContext.theory_of ctxt;
    1.23      val certT = Thm.ctyp_of thy;
    1.24 @@ -439,7 +439,7 @@
    1.25      val (insts, ctxt') = import_inst is_open ts ctxt;
    1.26    in (Proofterm.instantiate insts prf, ctxt') end;
    1.27  
    1.28 -fun import_thms is_open ths ctxt =
    1.29 +fun import is_open ths ctxt =
    1.30    let
    1.31      val thy = ProofContext.theory_of ctxt;
    1.32      val cert = Thm.cterm_of thy;
    1.33 @@ -457,8 +457,8 @@
    1.34    let val ((_, ths'), ctxt') = imp ths ctxt
    1.35    in exp ctxt' ctxt (f ctxt' ths') end;
    1.36  
    1.37 -val tradeT = gen_trade importT_thms exportT;
    1.38 -val trade = gen_trade (import_thms true) export;
    1.39 +val tradeT = gen_trade importT exportT;
    1.40 +val trade = gen_trade (import true) export;
    1.41  
    1.42  
    1.43  (* focus on outermost parameters *)