--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Sun Jul 05 15:02:30 2015 +0200
@@ -570,14 +570,14 @@
diff (Proof_Context.theory_of ctxt) (scheme_t, instance_t)
(*valuation of type variables*)
- val typeval = map (apply2 (Thm.ctyp_of ctxt)) type_pairing
+ val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
val typeval_env =
map (apfst dest_TVar) type_pairing
(*valuation of term variables*)
val termval =
- map (apfst (type_devar typeval_env)) term_pairing
- |> map (apply2 (Thm.cterm_of ctxt))
+ map (apfst (dest_Var o type_devar typeval_env)) term_pairing
+ |> map (apsnd (Thm.cterm_of ctxt))
in
Thm.instantiate (typeval, termval) scheme_thm
end