# HG changeset patch
# User wenzelm
# Date 1546527569 -3600
# Node ID 9da36603e5230fd84f4508f433b7dfdf11d2867b
# Parent  015f43ee4bb7fdf24cf8f54a99ca58c09c2c94bf
tuned;

diff -r 015f43ee4bb7 -r 9da36603e523 src/HOL/Tools/Argo/argo_tactic.ML
--- a/src/HOL/Tools/Argo/argo_tactic.ML	Thu Jan 03 15:55:48 2019 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Thu Jan 03 15:59:29 2019 +0100
@@ -79,9 +79,9 @@
 
 val timeout = Attrib.setup_config_real \<^binding>\<open>argo_timeout\<close> (K 10.0)
 
-val time_of_timeout = Time.fromReal o Config.apply timeout
+val timeout_seconds = seconds o Config.apply timeout
 
-fun with_timeout ctxt f x = Timeout.apply (time_of_timeout ctxt) f x
+fun with_timeout ctxt f x = Timeout.apply (timeout_seconds ctxt) f x
 
 
 (* extending the tactic *)