tuned signature;

--- a/src/Pure/ML/ml_antiquote.ML	Sun May 12 17:56:53 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Sun May 12 18:20:16 2013 +0200
@@ -68,7 +68,7 @@
   inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
 
   value (Binding.name "option_default") (Scan.lift Args.name >> (fn name =>
-    let val typ = Options.typ (Options.default ()) name
+    let val typ = Options.default_typ name
     in "fn () => Options.default_" ^ typ ^ " " ^ ML_Syntax.print_string name end)) #>
 
   value (Binding.name "binding")

--- a/src/Pure/ProofGeneral/preferences.ML	Sun May 12 17:56:53 2013 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sun May 12 18:20:16 2013 +0200
@@ -58,8 +58,7 @@
 
 fun options_pref option_name pgip_name descr : preference =
   let
-    val options = Options.default ();
-    val typ = Options.typ options option_name;
+    val typ = Options.default_typ option_name;
     val pgiptype =
       if typ = Options.boolT then PgipTypes.Pgipbool
       else if typ = Options.intT then PgipTypes.Pgipint (NONE, NONE)

--- a/src/Pure/System/options.ML	Sun May 12 17:56:53 2013 +0200
+++ b/src/Pure/System/options.ML	Sun May 12 18:20:16 2013 +0200
@@ -26,6 +26,7 @@
   val update: string -> string -> T -> T
   val decode: XML.body -> T
   val default: unit -> T
+  val default_typ: string -> string
   val default_bool: string -> bool
   val default_int: string -> int
   val default_real: string -> real
@@ -159,6 +160,7 @@
     SOME options => options
   | NONE => err_no_default ());
 
+fun default_typ name = typ (default ()) name;
 fun default_bool name = bool (default ()) name;
 fun default_int name = int (default ()) name;
 fun default_real name = real (default ()) name;