# HG changeset patch
# User wenzelm
# Date 1251476347 -7200
# Node ID de3727f1cf126a9875f34fd481d168931942b6d5
# Parent  54758ca53fd6f16951032fe1b54d45baa79da01f
removed obsolete print_ctyp, print_cterm;

diff -r 54758ca53fd6 -r de3727f1cf12 src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Aug 28 18:18:30 2009 +0200
+++ b/src/Pure/display.ML	Fri Aug 28 18:19:07 2009 +0200
@@ -29,10 +29,8 @@
   val pretty_thms: Proof.context -> thm list -> Pretty.T
   val pretty_ctyp: ctyp -> Pretty.T
   val string_of_ctyp: ctyp -> string
-  val print_ctyp: ctyp -> unit
   val pretty_cterm: cterm -> Pretty.T
   val string_of_cterm: cterm -> string
-  val print_cterm: cterm -> unit
   val print_syntax: theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T list
 end;
@@ -125,11 +123,9 @@
 
 fun pretty_ctyp cT = Syntax.pretty_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
 fun string_of_ctyp cT = Syntax.string_of_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-val print_ctyp = writeln o string_of_ctyp;
 
 fun pretty_cterm ct = Syntax.pretty_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
 fun string_of_cterm ct = Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
-val print_cterm = writeln o string_of_cterm;