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