src/Pure/Isar/isar_thy.ML

--- a/src/Pure/Isar/isar_thy.ML	Wed May 24 19:09:36 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed May 24 19:09:50 2000 +0200
@@ -135,8 +135,9 @@
     -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
     * Comment.text -> Toplevel.transition -> Toplevel.transition
+  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
-  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
+  val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
@@ -438,16 +439,17 @@
 (* local endings *)
 
 val local_qed =
-  proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest;
+  proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest;
 
 fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y);
 
 val local_terminal_proof =
   proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests;
 
+val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
 val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
-val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
 val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
+val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
 
 
 (* global endings *)
@@ -459,19 +461,21 @@
     val (thy, res as {kind, name, thm}) = finish state;
   in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end);
 
-val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest;
+val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest;
 val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
+val global_default_proof = global_result Method.global_default_proof;
 val global_immediate_proof = global_result Method.global_immediate_proof;
-val global_default_proof = global_result Method.global_default_proof;
 val global_skip_proof = global_result SkipProof.global_skip_proof;
+val global_done_proof = global_result Method.global_done_proof;
 
 
 (* common endings *)
 
 fun qed (meth, comment) = local_qed meth o global_qed meth;
 fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths;
+fun default_proof comment = local_default_proof o global_default_proof;
 fun immediate_proof comment = local_immediate_proof o global_immediate_proof;
-fun default_proof comment = local_default_proof o global_default_proof;
+fun done_proof comment = local_done_proof o global_done_proof;
 fun skip_proof comment = local_skip_proof o global_skip_proof;
 
 fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);