# HG changeset patch
# User wenzelm
# Date 931538835 -7200
# Node ID 13399b560e4e9554136426995859b285d2798752
# Parent  ab6d35b7283f6615dc0be535bbd2710c83779906
global_qed: removed alt_name, alt_att;

diff -r ab6d35b7283f -r 13399b560e4e src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Jul 09 18:46:51 1999 +0200
+++ b/src/Pure/Isar/method.ML	Fri Jul 09 18:47:15 1999 +0200
@@ -63,8 +63,7 @@
     -> Proof.state -> Proof.state Seq.seq
   val local_default_proof: ({kind: string, name: string, thm: thm} -> unit)
     -> Proof.state -> Proof.state Seq.seq
-  val global_qed: bstring option -> theory attribute list option -> text option
-    -> Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val global_qed: text option -> Proof.state -> theory * {kind: string, name: string, thm: thm}
   val global_terminal_proof: text * text option
     -> Proof.state -> theory * {kind: string, name: string, thm: thm}
   val global_immediate_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
@@ -312,12 +311,11 @@
 val local_default_proof = local_terminal_proof (default_text, None);
 
 
-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_qeds opt_text = Proof.global_qed (refine (if_none opt_text finish_text));
 
-fun global_qed alt_name alt_atts opt_text state =
+fun global_qed opt_text state =
   state
-  |> global_qeds alt_name alt_atts opt_text
+  |> global_qeds opt_text
   |> Proof.check_result "Failed to finish proof" state
   |> Seq.hd;
 
@@ -325,7 +323,7 @@
   state
   |> proof (Some text)
   |> Proof.check_result "Terminal proof method failed" state
-  |> (Seq.flat o Seq.map (global_qeds None None opt_text))
+  |> (Seq.flat o Seq.map (global_qeds opt_text))
   |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
   |> Seq.hd;