made smlnj happy;
authorwenzelm
Tue, 23 May 2006 14:00:06 +0200
changeset 19703 9c84266e1d5f
parent 19702 2ab12e94156f
child 19704 9b2612b807ab
made smlnj happy;
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] @