diff -r 8121e11ed765 -r 01a4e15ee253 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Jul 14 12:28:12 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Jul 14 13:05:28 1999 +0200
@@ -113,15 +113,16 @@
   val end_block: ProofHistory.T -> ProofHistory.T
   val tac: Method.text -> ProofHistory.T -> ProofHistory.T
   val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
-  val proof: Comment.interest * (Method.text * Comment.interest) option
+  val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
   val kill_proof: ProofHistory.T -> theory
-  val qed: (Method.text * Comment.interest) option -> Toplevel.transition -> Toplevel.transition
-  val terminal_proof: (Method.text * Comment.interest) * (Method.text * Comment.interest) option
+  val qed: (Method.text * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
-  val immediate_proof: Toplevel.transition -> Toplevel.transition
-  val default_proof: Toplevel.transition -> Toplevel.transition
-  val skip_proof: Toplevel.transition -> Toplevel.transition
+  val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
+    * 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 skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
   val also_i: (thm list * Comment.interest) option * Comment.text
@@ -309,8 +310,8 @@
 val tac = ProofHistory.applys o Method.tac;
 val then_tac = ProofHistory.applys o Method.then_tac;
 
-val proof =
-  ProofHistory.applys o Method.proof o apsome Comment.ignore_interest o Comment.ignore_interest';
+val proof = ProofHistory.applys o Method.proof o
+  apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;
 
 
 (* print result *)
@@ -365,11 +366,11 @@
 
 (* common endings *)
 
-fun qed meth = local_qed meth o global_qed meth;
-fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths;
-val immediate_proof = local_immediate_proof o global_immediate_proof;
-val default_proof = local_default_proof o global_default_proof;
-val skip_proof = local_skip_proof o global_skip_proof;
+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 immediate_proof comment = local_immediate_proof o global_immediate_proof;
+fun default_proof comment = local_default_proof o global_default_proof;
+fun skip_proof comment = local_skip_proof o global_skip_proof;
 
 
 (* calculational proof commands *)