removed obsolete print_ctyp, print_cterm;
authorwenzelm
Fri, 28 Aug 2009 18:19:07 +0200
changeset 32430 de3727f1cf12
parent 32429 54758ca53fd6
child 32431 bcd14373ec30
removed obsolete print_ctyp, print_cterm;
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;