src/Pure/System/options.ML

--- 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;