src/HOL/Tools/try0.ML

 
 signature TRY0 =
 sig
   val try0N : string
   val noneN : string
-  val auto : bool Unsynchronized.ref
   val try0 :
     Time.time option -> string list * string list * string list * string list
     -> Proof.state -> bool
   val setup : theory -> theory
 end;

 
 val try0N = "try0"
 
 val noneN = "none"
 
-val auto = Unsynchronized.ref false
-
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_tracing
+  ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    auto
+    @{option auto_try0}
     "auto-try0"
     "Try standard proof methods"
 
 val default_timeout = seconds 5.0
 

     (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans)
 
 fun try_try0 auto =
   do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
 
-val setup = Try.register_tool (try0N, (30, auto, try_try0))
+val setup = Try.register_tool (try0N, (30, @{option auto_try0}, try_try0))
 
 end;