tuned;
authorwenzelm
Thu, 03 Jan 2019 15:59:29 +0100
changeset 69578 9da36603e523
parent 69577 015f43ee4bb7
child 69579 edea246cedb3
tuned;
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 *)