# HG changeset patch
# User wenzelm
# Date 1251486922 -7200
# Node ID 11661f4327bbe806d4a1d1176a59b44832dfdd10
# Parent  64f30bdd3ba1be08057692626b779336cfa663e5
discontinued Display.pretty_ctyp/cterm etc.;

diff -r 64f30bdd3ba1 -r 11661f4327bb NEWS
--- a/NEWS	Fri Aug 28 21:04:03 2009 +0200
+++ b/NEWS	Fri Aug 28 21:15:22 2009 +0200
@@ -181,6 +181,10 @@
 or even Display.pretty_thm_without_context as last resort.
 INCOMPATIBILITY.
 
+* Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use
+Syntax.pretty_typ/term directly, preferably with proper context
+instead of global theory.
+
 
 *** System ***
 
diff -r 64f30bdd3ba1 -r 11661f4327bb src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Aug 28 21:04:03 2009 +0200
+++ b/src/Pure/display.ML	Fri Aug 28 21:15:22 2009 +0200
@@ -27,10 +27,6 @@
   val string_of_thm_without_context: thm -> string
   val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
   val pretty_thms: Proof.context -> thm list -> Pretty.T
-  val pretty_ctyp: ctyp -> Pretty.T
-  val string_of_ctyp: ctyp -> string
-  val pretty_cterm: cterm -> Pretty.T
-  val string_of_cterm: cterm -> string
   val print_syntax: theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T list
 end;
@@ -119,15 +115,6 @@
 fun pretty_thms ctxt = pretty_thms_aux ctxt true;
 
 
-(* other printing commands *)
-
-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);
-
-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);
-
-
 
 (** print theory **)