| changeset 59058 | a78612c67ec0 |
| parent 51428 | 12e46440e391 |
| child 62505 | 9e2a65912111 |
--- a/src/Pure/Concurrent/par_exn.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Concurrent/par_exn.ML Wed Nov 26 20:05:34 2014 +0100 @@ -33,7 +33,7 @@ fun the_serial exn = Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN)); -val exn_ord = rev_order o int_ord o pairself the_serial; +val exn_ord = rev_order o int_ord o apply2 the_serial; (* parallel exceptions *)