--- a/src/HOL/Tools/try0.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/HOL/Tools/try0.ML Fri Jul 12 23:45:05 2013 +0200
@@ -8,7 +8,6 @@
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
@@ -24,12 +23,10 @@
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"
@@ -196,6 +193,6 @@
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;