src/Pure/sign.ML
changeset 20211 c7f907f41f7c
parent 20155 da0505518e69
child 20230 04cb2d917de5
     1.1 --- a/src/Pure/sign.ML	Wed Jul 26 00:44:48 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Jul 26 00:44:49 2006 +0200
     1.3 @@ -143,8 +143,6 @@
     1.4    val string_of_sort: theory -> sort -> string
     1.5    val string_of_classrel: theory -> class list -> string
     1.6    val string_of_arity: theory -> arity -> string
     1.7 -  val pprint_term: theory -> term -> pprint_args -> unit
     1.8 -  val pprint_typ: theory -> typ -> pprint_args -> unit
     1.9    val pp: theory -> Pretty.pp
    1.10    val arity_number: theory -> string -> int
    1.11    val arity_sorts: theory -> string -> sort -> sort list
    1.12 @@ -398,9 +396,6 @@
    1.13  val string_of_classrel = Pretty.string_of oo pretty_classrel;
    1.14  val string_of_arity = Pretty.string_of oo pretty_arity;
    1.15  
    1.16 -val pprint_term = (Pretty.pprint o Pretty.quote) oo pretty_term;
    1.17 -val pprint_typ = (Pretty.pprint o Pretty.quote) oo pretty_typ;
    1.18 -
    1.19  fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy,
    1.20    pretty_classrel thy, pretty_arity thy);
    1.21