--- a/src/Pure/proofterm.ML Wed Oct 16 16:47:21 2019 +0200
+++ b/src/Pure/proofterm.ML Wed Oct 16 21:55:17 2019 +0200
@@ -2222,7 +2222,13 @@
val export_proof =
if named orelse not (export_enabled ()) then no_export_proof
- else Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1);
+ else
+ Lazy.lazy (fn () =>
+ join_proof body' |> open_proof |> export_proof thy i prop1 handle exn =>
+ if Exn.is_interrupt exn then
+ raise Fail ("Interrupt: potential resource problems while exporting proof " ^
+ string_of_int i)
+ else Exn.reraise exn);
val theory_name = Context.theory_long_name thy;
val thm = (i, make_thm_node theory_name name prop1 body');