diff -r c272680df665 -r c54a53ef1873 src/Pure/PIDE/document_id.ML
--- a/src/Pure/PIDE/document_id.ML	Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/PIDE/document_id.ML	Mon Sep 05 23:11:00 2016 +0200
@@ -31,8 +31,8 @@
 val none = 0;
 val make = Counter.make ();
 
-val parse = Markup.parse_int;
-val print = Markup.print_int;
+val parse = Value.parse_int;
+val print = Value.print_int;
 
 end;