# HG changeset patch
# User wenzelm
# Date 1573226718 -3600
# Node ID 77580c977e0ca2370207e8ecade9368ab1c6be51
# Parent  aedd11603fb4b960043cdaef96018faea19978bf
more robust;

diff -r aedd11603fb4 -r 77580c977e0c src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Nov 08 16:11:09 2019 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Nov 08 16:25:18 2019 +0100
@@ -29,9 +29,11 @@
     fun ?? x = if b then SOME x else NONE;
     fun ax (prf as PAxm (s, prop, _)) Ts =
       if b then PAxm (s, prop, SOME Ts) else prf;
-    fun ty T = if b then
-        let val Type (_, [Type (_, [U, _]), _]) = T
-        in SOME U end
+    fun ty T =
+      if b then
+        (case T of
+          Type (_, [Type (_, [U, _]), _]) => SOME U
+        | _ => NONE)
       else NONE;
     val equal_intr_axm = ax Proofterm.equal_intr_axm [];
     val equal_elim_axm = ax Proofterm.equal_elim_axm [];