--- a/src/Pure/Isar/isar_cmd.ML Sun Jul 19 19:20:17 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Jul 19 19:24:04 2009 +0200
@@ -230,7 +230,7 @@
(* local endings *)
fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
+val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
val local_default_proof = Toplevel.proof Proof.local_default_proof;
val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
val local_done_proof = Toplevel.proof Proof.local_done_proof;