# HG changeset patch
# User wenzelm
# Date 878658362 -3600
# Node ID c41846a38e2034c8241283e8a506c5dcf7d95dc3
# Parent  dc1cf9db1e17fd24017b85638a9f774cbb5ef6a3
added pretty_ctyp;

diff -r dc1cf9db1e17 -r c41846a38e20 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Nov 04 16:21:52 1997 +0100
+++ b/src/Pure/display.ML	Tue Nov 04 16:46:02 1997 +0100
@@ -12,6 +12,7 @@
   val pprint_ctyp	: ctyp -> pprint_args -> unit
   val pprint_theory	: theory -> pprint_args -> unit
   val pprint_thm	: thm -> pprint_args -> unit
+  val pretty_ctyp	: ctyp -> Pretty.T
   val pretty_cterm	: cterm -> Pretty.T
   val pretty_thm	: thm -> Pretty.T
   val print_cterm	: cterm -> unit
@@ -74,6 +75,9 @@
 
 (* other printing commands *)
 
+fun pretty_ctyp cT =
+  let val {sign, T} = rep_ctyp cT in Sign.pretty_typ sign T end;
+
 fun pprint_ctyp cT =
   let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end;