--- 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;