src/Pure/display.ML
changeset 19703 9c84266e1d5f
parent 19702 2ab12e94156f
child 19806 f860b7a98445
     1.1 --- a/src/Pure/display.ML	Tue May 23 13:55:02 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Tue May 23 14:00:06 2006 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4      fun pretty_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
     1.5  
     1.6      fun pretty_finals reds = Pretty.block
     1.7 -      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o #1) reds));
     1.8 +      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds));
     1.9  
    1.10      fun pretty_reduct (lhs, rhs) = Pretty.block
    1.11        ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @