more robust: avoid looping Lazy.force due to misinterpreted interrupt;

--- 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');