src/Pure/Tools/build.ML
changeset 65948 de7888573ed7
parent 65936 aece72468de5
child 66048 d244a895da50
--- a/src/Pure/Tools/build.ML	Sat May 27 13:07:27 2017 +0200
+++ b/src/Pure/Tools/build.ML	Sat May 27 13:20:35 2017 +0200
@@ -225,7 +225,7 @@
     val _ =
       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
         build_session args
-      handle exn => (List.app (error_message o #2) (Runtime.exn_messages exn); Exn.reraise exn);
+      handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn);
     val _ = Options.reset_default ();
   in () end;