# HG changeset patch
# User wenzelm
# Date 1160519252 -7200
# Node ID 34cfe3bbeff4c87154ae0fb4850e8cf57cfd0db6
# Parent  802705101b2af75f73c703399370ae50d41757fe
Toplevel.end_proof;

diff -r 802705101b2a -r 34cfe3bbeff4 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Oct 11 00:27:31 2006 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Oct 11 00:27:32 2006 +0200
@@ -98,17 +98,12 @@
 
 (* global endings *)
 
-fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state =>
-  if can (Proof.assert_bottom true) state then
-    ending int state |> (fn ctxt' => (ctxt', ProofContext.theory_of ctxt'))
-  else raise Toplevel.UNDEF);
-
-fun global_qed m = global_ending (K (Proof.global_qed (m, true)));
-val global_terminal_proof = global_ending o K o Proof.global_terminal_proof;
-val global_default_proof = global_ending (K Proof.global_default_proof);
-val global_immediate_proof = global_ending (K Proof.global_immediate_proof);
-val global_skip_proof = global_ending Proof.global_skip_proof;
-val global_done_proof = global_ending (K Proof.global_done_proof);
+fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
+val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
+val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
+val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
+val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
+val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
 
 val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1);