| changeset 51990 | cc66addbba6d |
| parent 51988 | a9725750c53a |
| child 56465 | 6ad693903e22 |
--- a/src/Pure/System/options.ML Tue May 14 20:32:10 2013 +0200 +++ b/src/Pure/System/options.ML Tue May 14 20:46:09 2013 +0200 @@ -103,7 +103,7 @@ val put_bool = put boolT Markup.print_bool; val put_int = put intT Markup.print_int; -val put_real = put realT signed_string_of_real; +val put_real = put realT Markup.print_real; val put_string = put stringT I;