--- a/src/Pure/Isar/isar_thy.ML Fri Jul 02 15:04:12 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML Fri Jul 02 15:04:31 1999 +0200
@@ -7,6 +7,7 @@
signature ISAR_THY =
sig
+ val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
val add_text: Comment.text -> theory -> theory
val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
val add_chapter: Comment.text -> theory -> theory
@@ -154,6 +155,7 @@
(* formal comments *)
+fun add_txt comment prf = prf;
fun add_text comment thy = thy;
fun add_title title author date thy = thy;
val add_chapter = add_text;