src/Pure/Isar/isar_thy.ML
changeset 6885 1dcac1789759
parent 6879 70f8c0c34b8d
child 6888 d0c68ebdabc5
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jul 02 15:04:12 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Jul 02 15:04:31 1999 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature ISAR_THY =
     1.6  sig
     1.7 +  val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.8    val add_text: Comment.text -> theory -> theory
     1.9    val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
    1.10    val add_chapter: Comment.text -> theory -> theory
    1.11 @@ -154,6 +155,7 @@
    1.12  
    1.13  (* formal comments *)
    1.14  
    1.15 +fun add_txt comment prf = prf;
    1.16  fun add_text comment thy = thy;
    1.17  fun add_title title author date thy = thy;
    1.18  val add_chapter = add_text;