Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more uniform exceptions, like cterm_instantiate;
authorwenzelm
Sun, 26 Jul 2015 11:08:57 +0200
changeset 60782 ba81f7c40e2a
parent 60781 2da59cdf531c
child 60783 495bede1c4d9
more uniform exceptions, like cterm_instantiate;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- 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.*)
isabelle