diff -r 7d8e0e3c553b -r a9725750c53a src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Tue May 14 19:30:21 2013 +0200
+++ b/src/Pure/System/options.ML	Tue May 14 19:48:31 2013 +0200
@@ -98,7 +98,7 @@
 
 val bool = get boolT (try Markup.parse_bool);
 val int = get intT (try Markup.parse_int);
-val real = get realT Real.fromString;
+val real = get realT (try Markup.parse_real);
 val string = get stringT SOME;
 
 val put_bool = put boolT Markup.print_bool;