src/Pure/Isar/parse.ML

 val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
 fun maybe scan = underscore >> K NONE || scan >> SOME;
 
 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 >> (the o Real.fromString) || int >> Real.fromInt;
+val real = float_number >> Markup.parse_real || int >> Real.fromInt;
 
 val tag_name = group (fn () => "tag name") (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
 
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();