315 (*import fixes*) |
315 (*import fixes*) |
316 val (tvars, vars) = |
316 val (tvars, vars) = |
317 chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |
317 chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |
318 |>> map Logic.dest_type; |
318 |>> map Logic.dest_type; |
319 |
319 |
320 val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); |
320 val instT = |
321 val inst = |
321 fold2 (fn a => fn b => (case a of TVar v => Term_Subst.TVars.add (v, b) | _ => I)) |
|
322 tvars tfrees Term_Subst.TVars.empty; |
|
323 val cinstT = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT []; |
|
324 val cinst = |
322 map_filter |
325 map_filter |
323 (fn (Var (xi, T), t) => |
326 (fn (Var (xi, T), t) => |
324 SOME ((xi, Term_Subst.instantiateT instT T), |
327 SOME ((xi, Term_Subst.instantiateT instT T), |
325 Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) |
328 Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) |
326 | _ => NONE) (vars ~~ frees); |
329 | _ => NONE) (vars ~~ frees); |
327 val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result; |
330 val result' = Thm.instantiate (cinstT, cinst) result; |
328 |
331 |
329 (*import assumes/defines*) |
332 (*import assumes/defines*) |
330 val result'' = |
333 val result'' = |
331 (fold (curry op COMP) asms' result' |
334 (fold (curry op COMP) asms' result' |
332 handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms')) |
335 handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms')) |