| changeset 63806 | c54a53ef1873 |
| parent 62505 | 9e2a65912111 |
| child 71250 | bd93c71521a0 |
--- a/src/Pure/Concurrent/par_exn.ML Mon Sep 05 22:09:52 2016 +0200 +++ b/src/Pure/Concurrent/par_exn.ML Mon Sep 05 23:11:00 2016 +0200 @@ -31,7 +31,7 @@ in Exn_Properties.update (update_serial @ update_props) exn end; fun the_serial exn = - Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN)); + Value.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN)); val exn_ord = rev_order o int_ord o apply2 the_serial;