src/Pure/display.ML
changeset 26423 8408edac8f6b
parent 25405 7ac8c93be624
child 26626 c6231d64d264
     1.1 --- a/src/Pure/display.ML	Thu Mar 27 14:41:06 2008 +0100
     1.2 +++ b/src/Pure/display.ML	Thu Mar 27 14:41:07 2008 +0100
     1.3 @@ -28,9 +28,6 @@
     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: thm -> Pretty.T
    1.13 @@ -48,13 +45,6 @@
    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