--- a/src/Tools/try.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/Tools/try.ML Fri Jan 04 23:22:53 2019 +0100
@@ -97,7 +97,7 @@
(fn {keywords, command_name, ...} =>
if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then
SOME
- {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
+ {delay = SOME (seconds (Options.default_real \<^system_option>\<open>auto_time_start\<close>)),
pri = ~ weight,
persistent = true,
strict = true,
@@ -105,7 +105,7 @@
let
val state = Toplevel.proof_of st
|> Proof.map_context (Context_Position.set_visible false)
- val auto_time_limit = Options.default_real @{system_option auto_time_limit}
+ val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
in
if auto_time_limit > 0.0 then
(case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of