# HG changeset patch
# User wenzelm
# Date 876156069 -7200
# Node ID 0830d11b8916d0bab12dfdb8ae9ef97d2ad1f937
# Parent  3b15cda31c9703951e88715675bfed2e687c6e0a
now uses new Sign.pretty_sort;

diff -r 3b15cda31c97 -r 0830d11b8916 src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Oct 06 18:40:24 1997 +0200
+++ b/src/Pure/display.ML	Mon Oct 06 18:41:09 1997 +0200
@@ -45,7 +45,8 @@
       if hlen = 0 then []
       else if ! show_hyps then
         [Pretty.brk 2, Pretty.list "[" "]"
-          (map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort xshyps)]
+          (map (Sign.pretty_term sign) hyps @
+           map (Sign.pretty_sort sign) xshyps)]
       else
         [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
   in
@@ -151,7 +152,7 @@
 
     val pretty_term = Sign.pretty_term sign;
     val pretty_typ = Sign.pretty_typ sign;
-    val pretty_sort = Sign.pretty_sort;
+    val pretty_sort = Sign.pretty_sort sign;
 
     fun pretty_vars prtf (X, vs) = Pretty.block
       [Pretty.block (Pretty.commas (map Pretty.str vs)),