--- a/src/Pure/System/options.ML Sun May 12 20:30:34 2013 +0200
+++ b/src/Pure/System/options.ML Sun May 12 20:46:17 2013 +0200
@@ -96,13 +96,13 @@
(* internal lookup and update *)
-val bool = get boolT Bool.fromString;
-val int = get intT Int.fromString;
+val bool = get boolT (try Markup.parse_bool);
+val int = get intT (try Markup.parse_int);
val real = get realT Real.fromString;
val string = get stringT SOME;
-val put_bool = put boolT Bool.toString;
-val put_int = put intT signed_string_of_int;
+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_string = put stringT I;