# HG changeset patch
# User wenzelm
# Date 930843676 -7200
# Node ID b250da153b1e3c203691d2815bed5b7d7dacb719
# Parent  01866edde713ece8ebfa09500d8cad93cd1246c0
fixed backtracking of global_qed;

diff -r 01866edde713 -r b250da153b1e src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jul 01 17:40:48 1999 +0200
+++ b/src/Pure/Isar/method.ML	Thu Jul 01 17:41:16 1999 +0200
@@ -298,6 +298,7 @@
 val default_text = named_method "default";
 val finish_text = named_method "finish";
 
+
 fun proof opt_text state =
   state
   |> Proof.assert_backward
@@ -309,10 +310,24 @@
 val local_immediate_proof = local_terminal_proof (Basic (K same));
 val local_default_proof = local_terminal_proof default_text;
 
-fun global_qed alt_name alt_atts opt_text =
+
+fun global_qeds alt_name alt_atts opt_text =
   Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;
 
-fun global_terminal_proof text = Seq.hd o Seq.map (global_qed None None None) o proof (Some text);
+fun global_qed alt_name alt_atts opt_text state =
+  state
+  |> global_qeds alt_name alt_atts opt_text
+  |> Proof.check_result "Failed to finish proof" state
+  |> Seq.hd;
+
+fun global_terminal_proof text state =
+  state
+  |> proof (Some text)
+  |> Proof.check_result "Terminal proof method failed" state
+  |> (Seq.flat o Seq.map (global_qeds None None None))
+  |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
+  |> Seq.hd;
+
 val global_immediate_proof = global_terminal_proof (Basic (K same));
 val global_default_proof = global_terminal_proof default_text;