added pretty_cterm;
authorwenzelm
Tue Jul 22 17:46:35 1997 +0200 (1997-07-22)
changeset 3547977d58464d7f
parent 3546 de164676a202
child 3548 108d09eb3454
added pretty_cterm;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Tue Jul 22 17:45:42 1997 +0200
     1.2 +++ b/src/Pure/display.ML	Tue Jul 22 17:46:35 1997 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    val pprint_ctyp	: ctyp -> pprint_args -> unit
     1.5    val pprint_theory	: theory -> pprint_args -> unit
     1.6    val pprint_thm	: thm -> pprint_args -> unit
     1.7 +  val pretty_cterm	: cterm -> Pretty.T
     1.8    val pretty_thm	: thm -> Pretty.T
     1.9    val print_cterm	: cterm -> unit
    1.10    val print_ctyp	: ctyp -> unit
    1.11 @@ -79,6 +80,9 @@
    1.12  
    1.13  val print_ctyp = writeln o string_of_ctyp;
    1.14  
    1.15 +fun pretty_cterm ct =
    1.16 +  let val {sign, t, ...} = rep_cterm ct in Sign.pretty_term sign t end;
    1.17 +
    1.18  fun pprint_cterm ct =
    1.19    let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end;
    1.20