src/Pure/Isar/isar_cmd.ML
changeset 60695 044f8bb3dd30
parent 60405 990c9fea6773
child 61086 fc7ab11128dc
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 08 12:09:44 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 08 14:30:00 2015 +0200
     1.3 @@ -182,8 +182,6 @@
     1.4  val local_done_proof = Toplevel.proof Proof.local_done_proof;
     1.5  val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
     1.6  
     1.7 -val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
     1.8 -
     1.9  
    1.10  (* global endings *)
    1.11  
    1.12 @@ -194,12 +192,10 @@
    1.13  val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
    1.14  val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
    1.15  
    1.16 -val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1);
    1.17 -
    1.18  
    1.19  (* common endings *)
    1.20  
    1.21 -fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
    1.22 +fun qed m = local_qed m o global_qed m;
    1.23  fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
    1.24  val default_proof = local_default_proof o global_default_proof;
    1.25  val immediate_proof = local_immediate_proof o global_immediate_proof;