added string_of: text -> string;

--- a/src/Pure/Isar/comment.ML	Wed Sep 29 13:13:06 1999 +0200
+++ b/src/Pure/Isar/comment.ML	Wed Sep 29 13:48:35 1999 +0200
@@ -8,6 +8,7 @@
 signature COMMENT =
 sig
   type text
+  val string_of: text -> string
   val plain: string -> text
   val none: text
   val ignore: 'a * text -> 'a
@@ -25,6 +26,8 @@
 (** text **)
 
 datatype text = Text of string;
+
+fun string_of (Text s) = s;
 val plain = Text;
 val none = plain "";