--- 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 **)