diff -r 12af4942923d -r e7036e812702 src/Pure/display.ML
--- a/src/Pure/display.ML	Mon May 08 17:40:06 2006 +0200
+++ b/src/Pure/display.ML	Mon May 08 17:40:07 2006 +0200
@@ -28,6 +28,9 @@
 signature DISPLAY =
 sig
   include BASIC_DISPLAY
+  val raw_string_of_sort: sort -> string
+  val raw_string_of_typ: typ -> string
+  val raw_string_of_term: term -> string
   val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
   val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
   val pretty_thm_no_quote: thm -> Pretty.T
@@ -53,6 +56,13 @@
 structure Display: DISPLAY =
 struct
 
+(** raw output **)
+
+val raw_string_of_sort = Sign.string_of_sort ProtoPure.thy;
+val raw_string_of_typ = Sign.string_of_typ ProtoPure.thy;
+val raw_string_of_term = Sign.string_of_term ProtoPure.thy;
+
+
 
 (** print thm **)