# HG changeset patch
# User wenzelm
# Date 1563788370 -7200
# Node ID 9e53a98702b9d20f177a1acbab2bd561e26cd7f2
# Parent  59f16c087840dcb1bad57816fe3782cd5f42197f
clarified exception;

diff -r 59f16c087840 -r 9e53a98702b9 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 22 11:31:42 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 22 11:39:30 2019 +0200
@@ -799,7 +799,8 @@
       in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
   | term_of Ts (Hyp t) = Hypt $ t
   | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
-  | term_of Ts MinProof = MinProoft;
+  | term_of Ts MinProof = MinProoft
+  | term_of Ts (Promise (_, t, _)) = raise TERM ("Illegal proof promise", [t]);
 
 in