# HG changeset patch
# User wenzelm
# Date 930920671 -7200
# Node ID 1dcac1789759f1a30608f64a494e9530959412ff
# Parent  a05159fbead0788ac7525f19338cfe4bd275dc60
add_txt;

diff -r a05159fbead0 -r 1dcac1789759 src/Pure/Isar/isar_thy.ML
--- 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;