--- a/src/Pure/drule.ML Sat Jul 25 23:41:53 2015 +0200
+++ b/src/Pure/drule.ML Sun Jul 26 11:08:57 2015 +0200
@@ -788,7 +788,10 @@
val inst = args' |> map (fn ((xi, T), cu) =>
((xi, Envir.norm_type tyenv T),
Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu)));
- in instantiate_normalize (instT, inst) th end;
+ 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]);
(*Left-to-right replacements: tpairs = [..., (vi, ti), ...].
Instantiates distinct Vars by terms, inferring type instantiations.*)