# HG changeset patch
# User wenzelm
# Date 1571255717 -7200
# Node ID 62b3acc801ece9234bad2da6fc3c618c519b10a5
# Parent  9ff9559f1ee203704cfe9ff4ce420e7ee1c8f7d6
more robust: avoid looping Lazy.force due to misinterpreted interrupt;

diff -r 9ff9559f1ee2 -r 62b3acc801ec src/Pure/proofterm.ML
--- 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');