src/Pure/display.ML
changeset 19591 e7036e812702
parent 19521 cfdab6a91332
child 19642 ea7162f84677
     1.1 --- a/src/Pure/display.ML	Mon May 08 17:40:06 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Mon May 08 17:40:07 2006 +0200
     1.3 @@ -28,6 +28,9 @@
     1.4  signature DISPLAY =
     1.5  sig
     1.6    include BASIC_DISPLAY
     1.7 +  val raw_string_of_sort: sort -> string
     1.8 +  val raw_string_of_typ: typ -> string
     1.9 +  val raw_string_of_term: term -> string
    1.10    val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    1.11    val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
    1.12    val pretty_thm_no_quote: thm -> Pretty.T
    1.13 @@ -53,6 +56,13 @@
    1.14  structure Display: DISPLAY =
    1.15  struct
    1.16  
    1.17 +(** raw output **)
    1.18 +
    1.19 +val raw_string_of_sort = Sign.string_of_sort ProtoPure.thy;
    1.20 +val raw_string_of_typ = Sign.string_of_typ ProtoPure.thy;
    1.21 +val raw_string_of_term = Sign.string_of_term ProtoPure.thy;
    1.22 +
    1.23 +
    1.24  
    1.25  (** print thm **)
    1.26