# 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));