# HG changeset patch
# User wenzelm
# Date 1120050806 -7200
# Node ID 81ea5a085158131a11c3f6b7fd49d2bf3db9e45c
# Parent  e64fb2cf50cb2abc98ffcfcd706fdc9550840147
replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);

diff -r e64fb2cf50cb -r 81ea5a085158 src/Pure/install_pp.ML
--- a/src/Pure/install_pp.ML	Wed Jun 29 15:13:25 2005 +0200
+++ b/src/Pure/install_pp.ML	Wed Jun 29 15:13:26 2005 +0200
@@ -9,4 +9,4 @@
 install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp);
 install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
-install_pp (make_pp ["typ"] Syntax.simple_pprint_typ);
+install_pp (make_pp ["typ"] (Sign.pprint_typ ProtoPure.thy));