# HG changeset patch
# User wenzelm
# Date 1566559213 -7200
# Node ID 706dac15554ba09674cb7c446cf3f2baebda1630
# Parent  b85a12c2e2bff3e7ff54436bcb05e9acdc88ce3d
clarified signature: prefer total operations;

diff -r b85a12c2e2bf -r 706dac15554b src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Aug 21 20:08:50 2019 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Aug 23 13:20:13 2019 +0200
@@ -132,8 +132,6 @@
             | 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 b85a12c2e2bf -r 706dac15554b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Aug 21 20:08:50 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Aug 23 13:20:13 2019 +0200
@@ -31,7 +31,6 @@
      proof: proof}
   type oracle = string * term option
   type thm = serial * thm_node
-  exception MIN_PROOF
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
@@ -215,8 +214,6 @@
 type thm = serial * thm_node;
 val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
-exception MIN_PROOF;
-
 
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
@@ -1561,6 +1558,8 @@
 
 local
 
+exception MIN_PROOF of unit;
+
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));
 fun variables_of t = vars_of t @ frees_of t;
@@ -1776,7 +1775,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 = raise MIN_PROOF
+      | mk_cnstrts _ _ _ _ MinProof = raise MIN_PROOF ()
   in mk_cnstrts env [] [] Symtab.empty cprf end;
 
 
@@ -1848,7 +1847,7 @@
       map (apply2 (Envir.norm_term env)) ((t, prop') :: cs)
       |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
     val env' = solve thy cs' env
-  in thawf (norm_proof env' prf) end;
+  in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof;
 
 fun prop_of_atom prop Ts = subst_atomic_types
   (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
diff -r b85a12c2e2bf -r 706dac15554b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Aug 21 20:08:50 2019 +0200
+++ b/src/Pure/thm.ML	Fri Aug 23 13:20:13 2019 +0200
@@ -993,8 +993,7 @@
 
 (*identified PThm node*)
 fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
-  Proofterm.get_id shyps hyps prop (proof_of thm)
-    handle Proofterm.MIN_PROOF => NONE;
+  Proofterm.get_id shyps hyps prop (proof_of thm);
 
 (*dependencies of PThm node*)
 fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) =