# HG changeset patch
# User wenzelm
# Date 1148385606 -7200
# Node ID 9c84266e1d5fe1a6e21ae02161d928e248e2df18
# Parent  2ab12e94156fbe8bfd3d05c88d3ca295b38cbaa7
made smlnj happy;

diff -r 2ab12e94156f -r 9c84266e1d5f src/Pure/display.ML
--- a/src/Pure/display.ML	Tue May 23 13:55:02 2006 +0200
+++ b/src/Pure/display.ML	Tue May 23 14:00:06 2006 +0200
@@ -208,7 +208,7 @@
     fun pretty_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
 
     fun pretty_finals reds = Pretty.block
-      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o #1) reds));
+      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds));
 
     fun pretty_reduct (lhs, rhs) = Pretty.block
       ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @