# HG changeset patch
# User wenzelm
# Date 869586395 -7200
# Node ID 977d58464d7f3281c32102b0d3861d97c691a0e4
# Parent  de164676a2023620f85e7ee4df1c60035d8719b8
added pretty_cterm;

diff -r de164676a202 -r 977d58464d7f 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;