renamed Variable.importT to importT_thms;
authorwenzelm
Wed Apr 04 23:29:41 2007 +0200 (2007-04-04)
changeset 22601948f23d4af29
parent 22600 043232f8dde2
child 22602 a165d9ed08b8
renamed Variable.importT to importT_thms;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Wed Apr 04 23:29:40 2007 +0200
     1.2 +++ b/src/Pure/variable.ML	Wed Apr 04 23:29:41 2007 +0200
     1.3 @@ -48,7 +48,7 @@
     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: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
     1.8 +  val importT_thms: 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      ((ctyp list * cterm list) * thm list) * Proof.context
    1.12 @@ -377,7 +377,7 @@
    1.13    let val (inst, ctxt') = import_inst is_open ts ctxt
    1.14    in (map (TermSubst.instantiate inst) ts, ctxt') end;
    1.15  
    1.16 -fun importT ths ctxt =
    1.17 +fun importT_thms ths ctxt =
    1.18    let
    1.19      val thy = ProofContext.theory_of ctxt;
    1.20      val certT = Thm.ctyp_of thy;
    1.21 @@ -410,7 +410,7 @@
    1.22    let val ((_, ths'), ctxt') = imp ths ctxt
    1.23    in exp ctxt' ctxt (f ctxt' ths') end;
    1.24  
    1.25 -val tradeT = gen_trade importT exportT;
    1.26 +val tradeT = gen_trade importT_thms exportT;
    1.27  val trade = gen_trade (import_thms true) export;
    1.28  
    1.29