src/Pure/variable.ML

   val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
   val import_inst: bool -> term list -> Proof.context ->
     (((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: thm list -> Proof.context -> ((ctyp * ctyp) list * thm list) * Proof.context
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import: bool -> thm list -> Proof.context ->
-    ((ctyp list * cterm list) * thm list) * Proof.context
+    (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   val warn_extra_tfrees: Proof.context -> Proof.context -> unit

   in (map (Term_Subst.instantiate inst) ts, ctxt') end;
 
 fun importT ths ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
-    val certT = Thm.ctyp_of thy;
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
-    val ths' = map (Thm.instantiate (instT', [])) ths;
-  in ((map #2 instT', ths'), ctxt') end;
+    val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
+    val ths' = map (Thm.instantiate insts') ths;
+  in ((instT', ths'), ctxt') end;
 
 fun import_prf is_open prf ctxt =
   let
     val ts = rev (Proofterm.fold_proof_terms cons (cons o Logic.mk_type) prf []);
     val (insts, ctxt') = import_inst is_open ts ctxt;
   in (Proofterm.instantiate insts prf, ctxt') end;
 
 fun import is_open ths ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
-    val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
-    val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst;
-    val ths' = map (Thm.instantiate (instT', inst')) ths;
-  in (((map #2 instT', map #2 inst'), ths'), ctxt') end;
+    val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
+    val insts' = Thm.certify_inst thy insts;
+    val ths' = map (Thm.instantiate insts') ths;
+  in ((insts', ths'), ctxt') end;
 
 
 (* import/export *)
 
 fun gen_trade imp exp f ctxt ths =