--- a/src/Pure/drule.ML Mon Jul 27 14:56:06 2015 +0200
+++ b/src/Pure/drule.ML Mon Jul 27 15:13:05 2015 +0200
@@ -743,12 +743,15 @@
(*instantiation with type-inference for variables*)
fun infer_instantiate_types _ [] th = th
- | infer_instantiate_types ctxt args th =
+ | infer_instantiate_types ctxt args raw_th =
let
val thy = Proof_Context.theory_of ctxt;
+ val th = Thm.transfer thy raw_th;
fun infer ((xi, T), cu) (tyenv, maxidx) =
let
+ val _ = Thm.ctyp_of ctxt T;
+ val _ = Thm.transfer_cterm thy cu;
val U = Thm.typ_of_cterm cu;
val maxidx' = maxidx
|> Integer.max (#2 xi)
@@ -778,9 +781,9 @@
((xi, Envir.norm_type tyenv T),
Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu)));
in instantiate_normalize (instT, inst) th end
- handle CTERM (msg, _) => raise THM (msg, 0, [th])
- | TERM (msg, _) => raise THM (msg, 0, [th])
- | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
+ handle CTERM (msg, _) => raise THM (msg, 0, [raw_th])
+ | TERM (msg, _) => raise THM (msg, 0, [raw_th])
+ | TYPE (msg, _, _) => raise THM (msg, 0, [raw_th]);
fun infer_instantiate _ [] th = th
| infer_instantiate ctxt args th =