# HG changeset patch
# User wenzelm
# Date 1437901737 -7200
# Node ID ba81f7c40e2ae04952e691c8373f6268b26144e6
# Parent  2da59cdf531c91c44cb416f677c597ec0121122f
more uniform exceptions, like cterm_instantiate;

diff -r 2da59cdf531c -r ba81f7c40e2a src/Pure/drule.ML
--- 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.*)