--- a/src/Pure/Isar/parse.ML Mon Sep 05 22:09:52 2016 +0200
+++ b/src/Pure/Isar/parse.ML Mon Sep 05 23:11:00 2016 +0200
@@ -217,7 +217,7 @@
val nat = number >> (#1 o Library.read_int o Symbol.explode);
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
-val real = float_number >> Markup.parse_real || int >> Real.fromInt;
+val real = float_number >> Value.parse_real || int >> Real.fromInt;
val tag_name = group (fn () => "tag name") (short_ident || string);
val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);