removed obsolete print_ctyp, print_cterm;
authorwenzelm
Fri Aug 28 18:19:07 2009 +0200 (2009-08-28)
changeset 32430de3727f1cf12
parent 32429 54758ca53fd6
child 32431 bcd14373ec30
removed obsolete print_ctyp, print_cterm;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Fri Aug 28 18:18:30 2009 +0200
     1.2 +++ b/src/Pure/display.ML	Fri Aug 28 18:19:07 2009 +0200
     1.3 @@ -29,10 +29,8 @@
     1.4    val pretty_thms: Proof.context -> thm list -> Pretty.T
     1.5    val pretty_ctyp: ctyp -> Pretty.T
     1.6    val string_of_ctyp: ctyp -> string
     1.7 -  val print_ctyp: ctyp -> unit
     1.8    val pretty_cterm: cterm -> Pretty.T
     1.9    val string_of_cterm: cterm -> string
    1.10 -  val print_cterm: cterm -> unit
    1.11    val print_syntax: theory -> unit
    1.12    val pretty_full_theory: bool -> theory -> Pretty.T list
    1.13  end;
    1.14 @@ -125,11 +123,9 @@
    1.15  
    1.16  fun pretty_ctyp cT = Syntax.pretty_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.17  fun string_of_ctyp cT = Syntax.string_of_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.18 -val print_ctyp = writeln o string_of_ctyp;
    1.19  
    1.20  fun pretty_cterm ct = Syntax.pretty_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.21  fun string_of_cterm ct = Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.22 -val print_cterm = writeln o string_of_cterm;
    1.23  
    1.24  
    1.25