# HG changeset patch
# User wenzelm
# Date 1350155360 -7200
# Node ID f222a054342e0f95d6934378ad9a106730be1792
# Parent  ed5080c031651d60185826ef91c387b96d499a4c
more informative error of initial/terminal proof steps;

diff -r ed5080c03165 -r f222a054342e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Oct 13 19:53:04 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Oct 13 21:09:20 2012 +0200
@@ -983,8 +983,27 @@
 
 (* concluding steps *)
 
+local
+
+fun failure_initial state =
+  let
+    val (ctxt, (facts, goal)) = get_goal state;
+    val pr_facts =
+      if null facts then ""
+      else Pretty.string_of (Pretty.big_list "facts:" (map (Display.pretty_thm ctxt) facts)) ^ "\n";
+    val pr_goal =
+      "goal:\n" ^ Pretty.string_of (Goal_Display.pretty_goal {main = false, limit = false} ctxt goal);
+  in error ("Failure of initial proof method on goal state:\n" ^ pr_facts ^ pr_goal) end;
+
+fun failure_terminal _ = error "Failure of terminal proof method";
+
+val op ORELSE = Seq.ORELSE;
+
 fun terminal_proof qeds initial terminal =
-  proof (SOME initial) #> Seq.maps (qeds terminal) #> the_finished_goal;
+  (((proof (SOME initial) ORELSE failure_initial)
+    #> Seq.maps (qeds terminal)) ORELSE failure_terminal) #> the_finished_goal;
+
+in
 
 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
 val local_default_proof = local_terminal_proof (Method.default_text, NONE);
@@ -998,6 +1017,8 @@
 fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
 val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
 
+end;
+
 
 (* common goal statements *)