| changeset 51988 | a9725750c53a |
| parent 51978 | 237ee582d663 |
| child 51990 | cc66addbba6d |
--- 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;