src/Pure/display.ML
changeset 32433 11661f4327bb
parent 32430 de3727f1cf12
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/display.ML	Fri Aug 28 21:04:03 2009 +0200
     1.2 +++ b/src/Pure/display.ML	Fri Aug 28 21:15:22 2009 +0200
     1.3 @@ -27,10 +27,6 @@
     1.4    val string_of_thm_without_context: thm -> string
     1.5    val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
     1.6    val pretty_thms: Proof.context -> thm list -> Pretty.T
     1.7 -  val pretty_ctyp: ctyp -> Pretty.T
     1.8 -  val string_of_ctyp: ctyp -> string
     1.9 -  val pretty_cterm: cterm -> Pretty.T
    1.10 -  val string_of_cterm: cterm -> string
    1.11    val print_syntax: theory -> unit
    1.12    val pretty_full_theory: bool -> theory -> Pretty.T list
    1.13  end;
    1.14 @@ -119,15 +115,6 @@
    1.15  fun pretty_thms ctxt = pretty_thms_aux ctxt true;
    1.16  
    1.17  
    1.18 -(* other printing commands *)
    1.19 -
    1.20 -fun pretty_ctyp cT = Syntax.pretty_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.21 -fun string_of_ctyp cT = Syntax.string_of_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.22 -
    1.23 -fun pretty_cterm ct = Syntax.pretty_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.24 -fun string_of_cterm ct = Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.25 -
    1.26 -
    1.27  
    1.28  (** print theory **)
    1.29