Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
now uses new Sign.pretty_sort;
authorwenzelm
Mon, 06 Oct 1997 18:41:09 +0200
changeset 3785 0830d11b8916
parent 3784 3b15cda31c97
child 3786 d5655489867c
now uses new Sign.pretty_sort;
src/Pure/display.ML file | annotate | diff | comparison | revisions 
--- 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)),
isabelle