diff -r 043232f8dde2 -r 948f23d4af29 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Apr 04 23:29:40 2007 +0200
+++ b/src/Pure/variable.ML	Wed Apr 04 23:29:41 2007 +0200
@@ -48,7 +48,7 @@
     (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
-  val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
+  val importT_thms: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import_thms: bool -> thm list -> Proof.context ->
     ((ctyp list * cterm list) * thm list) * Proof.context
@@ -377,7 +377,7 @@
   let val (inst, ctxt') = import_inst is_open ts ctxt
   in (map (TermSubst.instantiate inst) ts, ctxt') end;
 
-fun importT ths ctxt =
+fun importT_thms ths ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
@@ -410,7 +410,7 @@
   let val ((_, ths'), ctxt') = imp ths ctxt
   in exp ctxt' ctxt (f ctxt' ths') end;
 
-val tradeT = gen_trade importT exportT;
+val tradeT = gen_trade importT_thms exportT;
 val trade = gen_trade (import_thms true) export;