| changeset 69576 | cfac69e7b962 |
| parent 67149 | e61557884799 |
| child 69578 | 9da36603e523 |
--- a/src/HOL/Tools/Argo/argo_tactic.ML Thu Jan 03 14:12:44 2019 +0100 +++ b/src/HOL/Tools/Argo/argo_tactic.ML Thu Jan 03 15:55:36 2019 +0100 @@ -79,7 +79,7 @@ val timeout = Attrib.setup_config_real \<^binding>\<open>argo_timeout\<close> (K 10.0) -fun time_of_timeout ctxt = Time.fromReal (Config.get ctxt timeout) +val time_of_timeout = Time.fromReal o Config.apply timeout fun with_timeout ctxt f x = Timeout.apply (time_of_timeout ctxt) f x