src/Pure/display.ML
changeset 20211 c7f907f41f7c
parent 20076 def4ad161528
child 20226 6ea469c03314
     1.1 --- a/src/Pure/display.ML	Wed Jul 26 00:44:48 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Wed Jul 26 00:44:49 2006 +0200
     1.3 @@ -38,11 +38,8 @@
     1.4    val pretty_thms: thm list -> Pretty.T
     1.5    val pretty_thm_sg: theory -> thm -> Pretty.T
     1.6    val pretty_thms_sg: theory -> thm list -> Pretty.T
     1.7 -  val pprint_thm: thm -> pprint_args -> unit
     1.8    val pretty_ctyp: ctyp -> Pretty.T
     1.9 -  val pprint_ctyp: ctyp -> pprint_args -> unit
    1.10    val pretty_cterm: cterm -> Pretty.T
    1.11 -  val pprint_cterm: cterm -> pprint_args -> unit
    1.12    val pretty_full_theory: theory -> Pretty.T list
    1.13    val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list
    1.14    val pretty_goals: int -> thm -> Pretty.T list
    1.15 @@ -111,7 +108,6 @@
    1.16  
    1.17  
    1.18  val string_of_thm = Pretty.string_of o pretty_thm;
    1.19 -val pprint_thm = Pretty.pprint o pretty_thm;
    1.20  
    1.21  fun pretty_thms [th] = pretty_thm th
    1.22    | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    1.23 @@ -135,9 +131,6 @@
    1.24  fun pretty_ctyp cT =
    1.25    let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end;
    1.26  
    1.27 -fun pprint_ctyp cT =
    1.28 -  let val {thy, T, ...} = rep_ctyp cT in Sign.pprint_typ thy T end;
    1.29 -
    1.30  fun string_of_ctyp cT =
    1.31    let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end;
    1.32  
    1.33 @@ -146,9 +139,6 @@
    1.34  fun pretty_cterm ct =
    1.35    let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end;
    1.36  
    1.37 -fun pprint_cterm ct =
    1.38 -  let val {thy, t, ...} = rep_cterm ct in Sign.pprint_term thy t end;
    1.39 -
    1.40  fun string_of_cterm ct =
    1.41    let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end;
    1.42