--- a/src/Pure/PIDE/xml.ML Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/PIDE/xml.ML Mon Sep 05 23:11:00 2016 +0200
@@ -339,7 +339,7 @@
(* atomic values *)
fun int_atom s =
- Markup.parse_int s
+ Value.parse_int s
handle Fail _ => raise XML_ATOM s;
fun bool_atom "0" = false