# HG changeset patch
# User wenzelm
# Date 1248909280 -7200
# Node ID 4fb3f426052a94c9779a71ca6098ed69e988fb36
# Parent  e405636274199e08b3ac72a6c8a944d99a16487f
Variable.importT/import: return full instantiations, tuned;

diff -r e40563627419 -r 4fb3f426052a src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Jul 30 01:12:33 2009 +0200
+++ b/src/Pure/variable.ML	Thu Jul 30 01:14:40 2009 +0200
@@ -51,10 +51,10 @@
     (((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
@@ -427,11 +427,10 @@
 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
@@ -442,13 +441,10 @@
 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 *)