src/Pure/Isar/isar_cmd.ML
changeset 60403 9be917b2f376
parent 60378 26dcc7f19b02
child 60405 990c9fea6773
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 12:17:50 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 12:32:01 2015 +0200
     1.3 @@ -187,7 +187,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_future_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;
    1.12 @@ -199,7 +199,7 @@
    1.13  (* global endings *)
    1.14  
    1.15  fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
    1.16 -val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
    1.17 +val global_terminal_proof = Toplevel.end_proof o K o Proof.global_future_terminal_proof;
    1.18  val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
    1.19  val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
    1.20  val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;