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