# HG changeset patch
# User wenzelm
# Date 1566041968 -7200
# Node ID 2c7c8be65b7d0c5faaa1b088881603fb8b063c86
# Parent  61414c54a70c0a235618a0b053657057d15c7fe2
more robust, notably for open_proof of unnamed derivation;

diff -r 61414c54a70c -r 2c7c8be65b7d src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Sat Aug 17 13:24:40 2019 +0200
+++ b/src/Pure/Isar/runtime.ML	Sat Aug 17 13:39:28 2019 +0200
@@ -132,6 +132,8 @@
             | THM (msg, i, thms) =>
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: robust_context context Thm.string_of_thm thms)
+            | Proofterm.MIN_PROOF =>
+                raised exn "MIN_PROOF" ["minimal proof object in reconstruction"]
             | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
         in [((i, msg), id)] end)
       and sorted_msgs context exn =
diff -r 61414c54a70c -r 2c7c8be65b7d 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;
 
 
diff -r 61414c54a70c -r 2c7c8be65b7d src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 17 13:24:40 2019 +0200
+++ b/src/Pure/thm.ML	Sat Aug 17 13:39:28 2019 +0200
@@ -1007,7 +1007,8 @@
   Proofterm.get_approximative_name shyps hyps prop (proof_of thm);
 
 fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
-  Proofterm.get_id shyps hyps prop (proof_of thm);
+  Proofterm.get_id shyps hyps prop (proof_of thm)
+    handle Proofterm.MIN_PROOF => NONE;
 
 fun name_derivation name_pos =
   solve_constraints #> (fn thm as Thm (der, args) =>