1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed May 24 19:09:36 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed May 24 19:09:50 2000 +0200
     1.3 @@ -135,8 +135,9 @@
     1.4      -> Toplevel.transition -> Toplevel.transition
     1.5    val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
     1.6      * Comment.text -> Toplevel.transition -> Toplevel.transition
     1.7 +  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.8    val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.9 -  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    1.10 +  val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    1.11    val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    1.12    val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    1.13    val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
    1.14 @@ -438,16 +439,17 @@
    1.15  (* local endings *)
    1.16  
    1.17  val local_qed =
    1.18 -  proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest;
    1.19 +  proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest;
    1.20  
    1.21  fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y);
    1.22  
    1.23  val local_terminal_proof =
    1.24    proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests;
    1.25  
    1.26 +val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
    1.27  val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
    1.28 -val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
    1.29  val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
    1.30 +val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
    1.31  
    1.32  
    1.33  (* global endings *)
    1.34 @@ -459,19 +461,21 @@
    1.35      val (thy, res as {kind, name, thm}) = finish state;
    1.36    in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end);
    1.37  
    1.38 -val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest;
    1.39 +val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest;
    1.40  val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
    1.41 +val global_default_proof = global_result Method.global_default_proof;
    1.42  val global_immediate_proof = global_result Method.global_immediate_proof;
    1.43 -val global_default_proof = global_result Method.global_default_proof;
    1.44  val global_skip_proof = global_result SkipProof.global_skip_proof;
    1.45 +val global_done_proof = global_result Method.global_done_proof;
    1.46  
    1.47  
    1.48  (* common endings *)
    1.49  
    1.50  fun qed (meth, comment) = local_qed meth o global_qed meth;
    1.51  fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths;
    1.52 +fun default_proof comment = local_default_proof o global_default_proof;
    1.53  fun immediate_proof comment = local_immediate_proof o global_immediate_proof;
    1.54 -fun default_proof comment = local_default_proof o global_default_proof;
    1.55 +fun done_proof comment = local_done_proof o global_done_proof;
    1.56  fun skip_proof comment = local_skip_proof o global_skip_proof;
    1.57  
    1.58  fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);