src/Pure/Isar/method.ML
changeset 6872 b250da153b1e
parent 6849 0b660860c0ad
child 6934 04d051190a5f
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jul 01 17:40:48 1999 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jul 01 17:41:16 1999 +0200
     1.3 @@ -298,6 +298,7 @@
     1.4  val default_text = named_method "default";
     1.5  val finish_text = named_method "finish";
     1.6  
     1.7 +
     1.8  fun proof opt_text state =
     1.9    state
    1.10    |> Proof.assert_backward
    1.11 @@ -309,10 +310,24 @@
    1.12  val local_immediate_proof = local_terminal_proof (Basic (K same));
    1.13  val local_default_proof = local_terminal_proof default_text;
    1.14  
    1.15 -fun global_qed alt_name alt_atts opt_text =
    1.16 +
    1.17 +fun global_qeds alt_name alt_atts opt_text =
    1.18    Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;
    1.19  
    1.20 -fun global_terminal_proof text = Seq.hd o Seq.map (global_qed None None None) o proof (Some text);
    1.21 +fun global_qed alt_name alt_atts opt_text state =
    1.22 +  state
    1.23 +  |> global_qeds alt_name alt_atts opt_text
    1.24 +  |> Proof.check_result "Failed to finish proof" state
    1.25 +  |> Seq.hd;
    1.26 +
    1.27 +fun global_terminal_proof text state =
    1.28 +  state
    1.29 +  |> proof (Some text)
    1.30 +  |> Proof.check_result "Terminal proof method failed" state
    1.31 +  |> (Seq.flat o Seq.map (global_qeds None None None))
    1.32 +  |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
    1.33 +  |> Seq.hd;
    1.34 +
    1.35  val global_immediate_proof = global_terminal_proof (Basic (K same));
    1.36  val global_default_proof = global_terminal_proof default_text;
    1.37