src/Tools/try.ML
changeset 69593 3dda49e08b9d
parent 67149 e61557884799
child 74507 a241eadc0e3f
--- 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