src/Pure/proofterm.ML

--- a/src/Pure/proofterm.ML	Sat Aug 17 13:24:40 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 17 13:39:28 2019 +0200
@@ -37,6 +37,7 @@
 sig
   include BASIC_PROOFTERM
   val proofs: int Unsynchronized.ref
+  exception MIN_PROOF
   type pthm = proof_serial * thm_node
   type oracle = string * term option
   val proof_of: proof_body -> proof
@@ -213,6 +214,8 @@
 and thm_node =
   Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
 
+exception MIN_PROOF;
+
 type oracle = string * term option;
 val oracle_prop = the_default Term.dummy;
 
@@ -1821,7 +1824,7 @@
       | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
           mk_cnstrts_atom env vTs (oracle_prop prop) opTs prf
       | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
-      | mk_cnstrts _ _ _ _ MinProof = error "reconstruct_proof: minimal proof object"
+      | mk_cnstrts _ _ _ _ MinProof = raise MIN_PROOF
   in mk_cnstrts env [] [] Symtab.empty cprf end;