src/Pure/Isar/isar_cmd.ML
changeset 49012 8686c36fa27d
parent 48918 6e5fd4585512
child 49561 26fc70e983c2
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 30 19:18:49 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 30 21:23:04 2012 +0200
     1.3 @@ -265,7 +265,7 @@
     1.4  (* global endings *)
     1.5  
     1.6  fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
     1.7 -val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
     1.8 +val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
     1.9  val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
    1.10  val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
    1.11  val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;