# HG changeset patch
# User wenzelm
# Date 1555167372 -7200
# Node ID 8a23083ac0114e10b99056dbd39521b64341268c
# Parent  6218698851b9c65ff255d75504b461c675c416c2
prefer exception TYPE, e.g. when used within conversion;

diff -r 6218698851b9 -r 8a23083ac011 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Apr 13 16:42:19 2019 +0200
+++ b/src/Pure/thm.ML	Sat Apr 13 16:56:12 2019 +0200
@@ -175,9 +175,14 @@
       map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts
   | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);
 
-fun dest_ctyp_nth i (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) =
-      Ctyp {cert = cert, T = nth Ts i, maxidx = maxidx, sorts = sorts}
-  | dest_ctyp_nth _ cT = raise TYPE ("dest_ctyp_nth", [typ_of cT], []);
+fun dest_ctyp_nth i (Ctyp {cert, T, maxidx, sorts}) =
+  let fun err () = raise TYPE ("dest_ctyp_nth", [T], []) in
+    (case T of
+      Type (_, Ts) =>
+        Ctyp {cert = cert, T = nth Ts i handle General.Subscript => err (),
+          maxidx = maxidx, sorts = sorts}
+    | _ => err ())
+  end;