src/Pure/ML/ml_antiquote.ML

 
  (inline (Binding.name "assert")
     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
 
   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
+    in "fn () => Options.default_" ^ typ ^ " " ^ ML_Syntax.print_string name end)) #>
 
   value (Binding.name "binding")
     (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
 
   value (Binding.name "theory")