src/Pure/sign.ML
changeset 20211 c7f907f41f7c
parent 20155 da0505518e69
child 20230 04cb2d917de5
--- a/src/Pure/sign.ML	Wed Jul 26 00:44:48 2006 +0200
+++ b/src/Pure/sign.ML	Wed Jul 26 00:44:49 2006 +0200
@@ -143,8 +143,6 @@
   val string_of_sort: theory -> sort -> string
   val string_of_classrel: theory -> class list -> string
   val string_of_arity: theory -> arity -> string
-  val pprint_term: theory -> term -> pprint_args -> unit
-  val pprint_typ: theory -> typ -> pprint_args -> unit
   val pp: theory -> Pretty.pp
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
@@ -398,9 +396,6 @@
 val string_of_classrel = Pretty.string_of oo pretty_classrel;
 val string_of_arity = Pretty.string_of oo pretty_arity;
 
-val pprint_term = (Pretty.pprint o Pretty.quote) oo pretty_term;
-val pprint_typ = (Pretty.pprint o Pretty.quote) oo pretty_typ;
-
 fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy,
   pretty_classrel thy, pretty_arity thy);