src/Pure/display.ML
changeset 26626 c6231d64d264
parent 26423 8408edac8f6b
child 26637 0bfccafc52eb
     1.1 --- a/src/Pure/display.ML	Thu Apr 10 20:54:18 2008 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Apr 12 17:00:35 2008 +0200
     1.3 @@ -109,20 +109,12 @@
     1.4  
     1.5  (* other printing commands *)
     1.6  
     1.7 -fun pretty_ctyp cT =
     1.8 -  let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end;
     1.9 -
    1.10 -fun string_of_ctyp cT =
    1.11 -  let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end;
    1.12 -
    1.13 +fun pretty_ctyp cT = Sign.pretty_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.14 +fun string_of_ctyp cT = Sign.string_of_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.15  val print_ctyp = writeln o string_of_ctyp;
    1.16  
    1.17 -fun pretty_cterm ct =
    1.18 -  let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end;
    1.19 -
    1.20 -fun string_of_cterm ct =
    1.21 -  let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end;
    1.22 -
    1.23 +fun pretty_cterm ct = Sign.pretty_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.24 +fun string_of_cterm ct = Sign.string_of_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.25  val print_cterm = writeln o string_of_cterm;
    1.26  
    1.27