more uniform exceptions, like cterm_instantiate;
authorwenzelm
Sun Jul 26 11:08:57 2015 +0200 (2015-07-26)
changeset 60782ba81f7c40e2a
parent 60781 2da59cdf531c
child 60783 495bede1c4d9
more uniform exceptions, like cterm_instantiate;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Sat Jul 25 23:41:53 2015 +0200
     1.2 +++ b/src/Pure/drule.ML	Sun Jul 26 11:08:57 2015 +0200
     1.3 @@ -788,7 +788,10 @@
     1.4          val inst = args' |> map (fn ((xi, T), cu) =>
     1.5            ((xi, Envir.norm_type tyenv T),
     1.6              Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu)));
     1.7 -      in instantiate_normalize (instT, inst) th end;
     1.8 +      in instantiate_normalize (instT, inst) th end
     1.9 +      handle CTERM (msg, _) => raise THM (msg, 0, [th])
    1.10 +        | TERM (msg, _) => raise THM (msg, 0, [th])
    1.11 +        | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
    1.12  
    1.13  (*Left-to-right replacements: tpairs = [..., (vi, ti), ...].
    1.14    Instantiates distinct Vars by terms, inferring type instantiations.*)