src/Pure/display.ML

--- a/src/Pure/display.ML	Tue Jul 22 17:45:42 1997 +0200
+++ b/src/Pure/display.ML	Tue Jul 22 17:46:35 1997 +0200
@@ -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_cterm	: cterm -> Pretty.T
   val pretty_thm	: thm -> Pretty.T
   val print_cterm	: cterm -> unit
   val print_ctyp	: ctyp -> unit
@@ -79,6 +80,9 @@
 
 val print_ctyp = writeln o string_of_ctyp;
 
+fun pretty_cterm ct =
+  let val {sign, t, ...} = rep_cterm ct in Sign.pretty_term sign t end;
+
 fun pprint_cterm ct =
   let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end;