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 =