added pretty_ctyp;
authorwenzelm
Tue Nov 04 16:46:02 1997 +0100 (1997-11-04)
changeset 4126c41846a38e20
parent 4125 dc1cf9db1e17
child 4127 e0382d653d62
added pretty_ctyp;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Tue Nov 04 16:21:52 1997 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Nov 04 16:46:02 1997 +0100
     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_ctyp	: ctyp -> Pretty.T
     1.8    val pretty_cterm	: cterm -> Pretty.T
     1.9    val pretty_thm	: thm -> Pretty.T
    1.10    val print_cterm	: cterm -> unit
    1.11 @@ -74,6 +75,9 @@
    1.12  
    1.13  (* other printing commands *)
    1.14  
    1.15 +fun pretty_ctyp cT =
    1.16 +  let val {sign, T} = rep_ctyp cT in Sign.pretty_typ sign T end;
    1.17 +
    1.18  fun pprint_ctyp cT =
    1.19    let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end;
    1.20