# HG changeset patch
# User wenzelm
# Date 1003766486 -7200
# Node ID 427d80b807c74f1ca9f6efbdad96ad9511eef36f
# Parent  341b1fbc613043af4f4bd5db2376244ae9c83650
qualified names;

diff -r 341b1fbc6130 -r 427d80b807c7 src/Pure/install_pp.ML
--- a/src/Pure/install_pp.ML	Mon Oct 22 18:01:15 2001 +0200
+++ b/src/Pure/install_pp.ML	Mon Oct 22 18:01:26 2001 +0200
@@ -4,10 +4,10 @@
 Set up automatic toplevel pretty printing.
 *)
 
-install_pp (make_pp ["Theory", "theory"] pprint_theory);
-install_pp (make_pp ["Thm", "thm"] pprint_thm);
-install_pp (make_pp ["Thm", "cterm"] pprint_cterm);
-install_pp (make_pp ["Thm", "ctyp"] pprint_ctyp);
+install_pp (make_pp ["Theory", "theory"] Display.pprint_theory);
+install_pp (make_pp ["Thm", "thm"] Display.pprint_thm);
+install_pp (make_pp ["Thm", "cterm"] Display.pprint_cterm);
+install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp);
 install_pp (make_pp ["Sign", "sg"] Sign.pprint_sg);
 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
 install_pp (make_pp ["typ"] Syntax.simple_pprint_typ);