# HG changeset patch
# User wenzelm
# Date 1662633820 -7200
# Node ID 730638d4e37a85664d7b1fa1f0d6c7ee224a4766
# Parent  ae89a502b6fa237fe95d15c29de4da3f34ca0512
clarified failure: warning for logical error, exception for program breakdown;

diff -r ae89a502b6fa -r 730638d4e37a src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Sep 07 21:15:45 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Sep 08 12:43:40 2022 +0200
@@ -282,25 +282,29 @@
             ((fold o fold) Term.add_vars propss [] |> sort Term_Ord.var_ord |> map_filter inst);
         in if null prts then [] else [Pretty.big_list title (map inst_pair prts)] end;
 
-    fun prt_failed prt = [Pretty.block [Pretty.str title, Pretty.brk 1, prt]];
-
+    exception LOST_STRUCTURE;
     fun goal_matcher () =
       let
-        val concl = Logic.unprotect (Thm.concl_of goal);
+        val concl =
+          Logic.unprotect (Thm.concl_of goal)
+            handle TERM _ => raise LOST_STRUCTURE;
         val goal_propss = filter_out null propss;
         val results =
           Logic.dest_conjunction_balanced (length goal_propss) concl
-          |> map2 Logic.dest_conjunction_balanced (map length goal_propss);
+          |> map2 Logic.dest_conjunction_balanced (map length goal_propss)
+            handle TERM _ => raise LOST_STRUCTURE;
       in
         Unify.matcher (Context.Proof ctxt)
           (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (flat results)
       end;
+
+    fun failure msg = (warning (title ^ " " ^ msg); []);
   in
     if Config.get ctxt show_goal_inst then
-      (case Exn.interruptible_capture goal_matcher () of
-        Exn.Res (SOME env) => prt_inst env
-      | Exn.Res NONE => prt_failed (Pretty.mark_str (Markup.bad (), "FAILED"))
-      | Exn.Exn exn => prt_failed (Runtime.pretty_exn exn))
+      (case goal_matcher () of
+        SOME env => prt_inst env
+      | NONE => failure "match failed")
+      handle LOST_STRUCTURE => failure "lost goal structure"
     else []
   end;