diff --git a/src/HOL/Analysis/ex/Metric_Arith_Examples.thy b/src/HOL/Analysis/ex/Metric_Arith_Examples.thy
--- a/src/HOL/Analysis/ex/Metric_Arith_Examples.thy
+++ b/src/HOL/Analysis/ex/Metric_Arith_Examples.thy
@@ -1,103 +1,103 @@
 theory Metric_Arith_Examples
 imports "HOL-Analysis.Elementary_Metric_Spaces"
 begin
 
 
 text \<open>simple examples\<close>
 
 lemma "\<exists>x::'a::metric_space. x=x"
   by metric
 lemma "\<forall>(x::'a::metric_space). \<exists>y. x = y"
   by metric
 
 
 text \<open>reasoning with "dist x y = 0 \<longleftrightarrow> x = y"\<close>
 
 lemma "\<exists>x y. dist x y = 0"
   by metric
 
 lemma "\<exists>y. dist x y = 0"
   by metric
 
 lemma "0 = dist x y \<Longrightarrow> x = y"
   by metric
 
 lemma "x \<noteq> y \<Longrightarrow> dist x y \<noteq> 0"
   by metric
 
 lemma "\<exists>y. dist x y \<noteq> 1"
   by metric
 
 lemma "x = y \<longleftrightarrow> dist x x = dist y x \<and> dist x y = dist y y"
   by metric
 
 lemma "dist a b \<noteq> dist a c \<Longrightarrow> b \<noteq> c"
   by metric
 
 text \<open>reasoning with positive semidefiniteness\<close>
 
 lemma "dist y x + c \<ge> c"
   by metric
 
 lemma "dist x y + dist x z \<ge> 0"
   by metric
 
 lemma "dist x y \<ge> v \<Longrightarrow> dist x y + dist (a::'a) b \<ge> v" for x::"('a::metric_space)"
   by metric
 
 lemma "dist x y < 0 \<longrightarrow> P"
   by metric
 
 text \<open>reasoning with the triangle inequality\<close>
 
 lemma "dist a d \<le> dist a b + dist b c + dist c d"
   by metric
 
 lemma "dist a e \<le> dist a b + dist b c + dist c d + dist d e"
-  using [[argo_timeout = 25]] by metric
+  by metric
 
 lemma "max (dist x y) \<bar>dist x z - dist z y\<bar> = dist x y"
   by metric
 
 lemma
   "dist w x < e/3 \<Longrightarrow> dist x y < e/3 \<Longrightarrow> dist y z < e/3 \<Longrightarrow> dist w x < e"
   by metric
 
 lemma "dist w x < e/4 \<Longrightarrow> dist x y < e/4 \<Longrightarrow> dist y z < e/2 \<Longrightarrow> dist w z < e"
   by metric
 
 
 text \<open>more complex examples\<close>
 
 lemma "dist x y \<le> e \<Longrightarrow> dist x z \<le> e \<Longrightarrow> dist y z \<le> e
   \<Longrightarrow> p \<in> (cball x e \<union> cball y e \<union> cball z e) \<Longrightarrow> dist p x \<le> 2*e"
   by metric
 
 lemma hol_light_example:
   "\<not> disjnt (ball x r) (ball y s) \<longrightarrow>
     (\<forall>p q. p \<in> ball x r \<union> ball y s \<and> q \<in> ball x r \<union> ball y s \<longrightarrow> dist p q < 2 * (r + s))"
   unfolding disjnt_iff
   by metric
 
 lemma "dist x y \<le> e \<Longrightarrow> z \<in> ball x f \<Longrightarrow> dist z y < e + f"
   by metric
 
 lemma "dist x y = r / 2 \<Longrightarrow> (\<forall>z. dist x z < r / 4 \<longrightarrow> dist y z \<le> 3 * r / 4)"
   by metric
 
 lemma "s \<ge> 0 \<Longrightarrow> t \<ge> 0 \<Longrightarrow> z \<in> (ball x s) \<union> (ball y t) \<Longrightarrow> dist z y \<le> dist x y + s + t"
   by metric
 
 lemma "0 < r \<Longrightarrow> ball x r \<subseteq> ball y s \<Longrightarrow> ball x r \<subseteq> ball z t \<Longrightarrow> dist y z \<le> s + t"
   by metric
 
 
 text \<open>non-trivial quantifier structure\<close>
 
 lemma "\<exists>x. \<forall>r\<le>0. \<exists>z. dist x z \<ge> r"
   by metric
 
 lemma "\<And>a r x y. dist x a + dist a y = r \<Longrightarrow> \<forall>z. r \<le> dist x z + dist z y \<Longrightarrow> dist x y = r"
   by metric
 
 end
\ No newline at end of file
diff --git a/src/HOL/Analysis/metric_arith.ML b/src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML
+++ b/src/HOL/Analysis/metric_arith.ML
@@ -1,307 +1,311 @@
 (*  Title:      HOL/Analysis/metric_arith.ML
     Author:     Maximilian Schäffeler (port from HOL Light)
 
 A decision procedure for metric spaces.
 *)
 
 signature METRIC_ARITH =
 sig
   val trace: bool Config.T
+  val argo_timeout: real Config.T
   val metric_arith_tac : Proof.context -> int -> tactic
 end
 
 structure Metric_Arith : METRIC_ARITH =
 struct
 
 (* apply f to both cterms in ct_pair, merge results *)
 fun app_union_ct_pair f ct_pair = uncurry (union (op aconvc)) (apply2 f ct_pair)
 
 val trace = Attrib.setup_config_bool \<^binding>\<open>metric_trace\<close> (K false)
 
 fun trace_tac ctxt msg =
   if Config.get ctxt trace then print_tac ctxt msg else all_tac
 
-fun argo_trace_ctxt ctxt =
-  if Config.get ctxt trace
-  then Config.map (Argo_Tactic.trace) (K "basic") ctxt
-  else ctxt
+val argo_timeout = Attrib.setup_config_real \<^binding>\<open>metric_argo_timeout\<close> (K 20.0)
+
+fun argo_ctxt ctxt =
+  let
+    val ctxt1 =
+      if Config.get ctxt trace
+      then Config.map (Argo_Tactic.trace) (K "basic") ctxt
+      else ctxt
+  in Config.put Argo_Tactic.timeout (Config.get ctxt1 argo_timeout) ctxt1 end
 
 fun free_in v t =
   Term.exists_subterm (fn u => u aconv Thm.term_of v) (Thm.term_of t);
 
 (* build a cterm set with elements cts of type ty *)
 fun mk_ct_set ctxt ty =
   map Thm.term_of #>
   HOLogic.mk_set ty #>
   Thm.cterm_of ctxt
 
 fun prenex_tac ctxt =
   let
     val prenex_simps = Proof_Context.get_thms ctxt @{named_theorems metric_prenex}
     val prenex_ctxt = put_simpset HOL_basic_ss ctxt addsimps prenex_simps
   in
     simp_tac prenex_ctxt THEN'
     K (trace_tac ctxt "Prenex form")
   end
 
 fun nnf_tac ctxt =
   let
     val nnf_simps = Proof_Context.get_thms ctxt @{named_theorems metric_nnf}
     val nnf_ctxt = put_simpset HOL_basic_ss ctxt addsimps nnf_simps
   in
     simp_tac nnf_ctxt THEN'
     K (trace_tac ctxt "NNF form")
   end
 
 fun unfold_tac ctxt =
   asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (
     Proof_Context.get_thms ctxt @{named_theorems metric_unfold}))
 
 fun pre_arith_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps (
     Proof_Context.get_thms ctxt @{named_theorems metric_pre_arith})) THEN'
     K (trace_tac ctxt "Prepared for decision procedure")
 
 fun dist_refl_sym_tac ctxt =
   let
     val refl_sym_simps = @{thms dist_self dist_commute add_0_right add_0_left simp_thms}
     val refl_sym_ctxt = put_simpset HOL_basic_ss ctxt addsimps refl_sym_simps
   in
     simp_tac refl_sym_ctxt THEN'
     K (trace_tac ctxt ("Simplified using " ^ @{make_string} refl_sym_simps))
   end
 
 fun is_exists \<^Const_>\<open>Ex _ for _\<close> = true
   | is_exists \<^Const_>\<open>Trueprop for t\<close> = is_exists t
   | is_exists _ = false
 
 fun is_forall \<^Const_>\<open>All _ for _\<close> = true
   | is_forall \<^Const_>\<open>Trueprop for t\<close> = is_forall t
   | is_forall _ = false
 
 
 (* find all free points in ct of type metric_ty *)
 fun find_points ctxt metric_ty ct =
   let
     fun find ct =
       (if Thm.typ_of_cterm ct = metric_ty then [ct] else []) @
       (case Thm.term_of ct of
         _ $ _ => app_union_ct_pair find (Thm.dest_comb ct)
       | Abs _ =>
           (*ensure the point doesn't contain the bound variable*)
           let val (x, body) = Thm.dest_abs_global ct
           in filter_out (free_in x) (find body) end
       | _ => [])
   in
     (case find ct of
       [] =>
         (*if no point can be found, invent one*)
         let val x = singleton (Term.variant_frees (Thm.term_of ct)) ("x", metric_ty)
         in [Thm.cterm_of ctxt (Free x)] end
     | points => points)
   end
 
 (* find all cterms "dist x y" in ct, where x and y have type metric_ty *)
 fun find_dist metric_ty =
   let
     fun find ct =
       (case Thm.term_of ct of
         \<^Const_>\<open>dist T for _ _\<close> => if T = metric_ty then [ct] else []
       | _ $ _ => app_union_ct_pair find (Thm.dest_comb ct)
       | Abs _ =>
           let val (x, body) = Thm.dest_abs_global ct
           in filter_out (free_in x) (find body) end
       | _ => [])
   in find end
 
 (* find all "x=y", where x has type metric_ty *)
 fun find_eq metric_ty =
   let
     fun find ct =
       (case Thm.term_of ct of
         \<^Const_>\<open>HOL.eq T for _ _\<close> =>
           if T = metric_ty then [ct]
           else app_union_ct_pair find (Thm.dest_binop ct)
       | _ $ _ => app_union_ct_pair find (Thm.dest_comb ct)
       | Abs _ =>
           let val (x, body) = Thm.dest_abs_global ct
           in filter_out (free_in x) (find body) end
       | _ => [])
   in find end
 
 (* rewrite ct of the form "dist x y" using maxdist_thm *)
 fun maxdist_conv ctxt fset_ct ct =
   let
     val (x, y) = Thm.dest_binop ct
     val solve_prems =
       rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt
         addsimps @{thms finite.emptyI finite_insert empty_iff insert_iff})))
     val image_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms image_empty image_insert})
     val dist_refl_sym_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self})
     val algebra_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps
         @{thms diff_self diff_0_right diff_0 abs_zero abs_minus_cancel abs_minus_commute})
     val insert_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms insert_absorb2 insert_commute})
     val sup_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms cSup_singleton Sup_insert_insert})
     val real_abs_dist_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms real_abs_dist})
     val maxdist_thm =
       \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y and s = fset_ct in
         lemma \<open>finite s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> dist x y \<equiv> SUP a\<in>s. \<bar>dist x a - dist a y\<bar>\<close>
           for x y :: \<open>'a::metric_space\<close>
           by (fact maxdist_thm)\<close>
       |> solve_prems
   in
     ((Conv.rewr_conv maxdist_thm) then_conv
     (* SUP to Sup *)
     image_simp then_conv
     dist_refl_sym_simp then_conv
     algebra_simp then_conv
     (* eliminate duplicate terms in set *)
     insert_simp then_conv
     (* Sup to max *)
     sup_simp then_conv
     real_abs_dist_simp) ct
   end
 
 (* rewrite ct of the form "x=y" using metric_eq_thm *)
 fun metric_eq_conv ctxt fset_ct ct =
   let
     val (x, y) = Thm.dest_binop ct
     val solve_prems =
       rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt
         addsimps @{thms empty_iff insert_iff})))
     val ball_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps
         @{thms Set.ball_empty ball_insert})
     val dist_refl_sym_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self})
     val metric_eq_thm =
       \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y and s = fset_ct in
         lemma \<open>x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x = y \<equiv> \<forall>a\<in>s. dist x a = dist y a\<close>
           for x y :: \<open>'a::metric_space\<close>
           by (fact metric_eq_thm)\<close>
       |> solve_prems
   in
     ((Conv.rewr_conv metric_eq_thm) then_conv
     (*convert \<forall>x\<in>{x\<^sub>1,...,x\<^sub>n}. P x to P x\<^sub>1 \<and> ... \<and> P x\<^sub>n*)
     ball_simp then_conv
     dist_refl_sym_simp) ct
   end
 
 (* build list of theorems "0 \<le> dist x y" for all dist terms in ct *)
 fun augment_dist_pos metric_ty ct =
   let fun inst dist_ct =
     let val (x, y) = Thm.dest_binop dist_ct in
       \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y
         in lemma \<open>dist x y \<ge> 0\<close> for x y :: \<open>'a::metric_space\<close> by simp\<close>
     end
   in map inst (find_dist metric_ty ct) end
 
 (* apply maxdist_conv and metric_eq_conv to the goal, thereby embedding the goal in (\<real>\<^sup>n,dist\<^sub>\<infinity>) *)
 fun embedding_tac ctxt metric_ty = CSUBGOAL (fn (goal, i) =>
   let
     val points = find_points ctxt metric_ty goal
     val fset_ct = mk_ct_set ctxt metric_ty points
     (*embed all subterms of the form "dist x y" in (\<real>\<^sup>n,dist\<^sub>\<infinity>)*)
     val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty goal)
     (*replace point equality by equality of components in \<real>\<^sup>n*)
     val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty goal)
   in
     (K (trace_tac ctxt "Embedding into \<real>\<^sup>n") THEN'
       CONVERSION (Conv.top_sweep_rewrs_conv (eq1 @ eq2) ctxt)) i
   end)
 
 (* decision procedure for linear real arithmetic *)
 fun lin_real_arith_tac ctxt metric_ty = CSUBGOAL (fn (goal, i) =>
-  let
-    val dist_thms = augment_dist_pos metric_ty goal
-    val ctxt' = argo_trace_ctxt ctxt
-  in Argo_Tactic.argo_tac ctxt' dist_thms i end)
+  let val dist_thms = augment_dist_pos metric_ty goal
+  in Argo_Tactic.argo_tac (argo_ctxt ctxt) dist_thms i end)
 
 fun basic_metric_arith_tac ctxt metric_ty =
   SELECT_GOAL (
     dist_refl_sym_tac ctxt 1 THEN
     IF_UNSOLVED (embedding_tac ctxt metric_ty 1) THEN
     IF_UNSOLVED (pre_arith_tac ctxt 1) THEN
     IF_UNSOLVED (lin_real_arith_tac ctxt metric_ty 1))
 
 (* tries to infer the metric space from ct from dist terms,
    if no dist terms are present, equality terms will be used *)
 fun guess_metric ctxt tm =
   let
     val thy = Proof_Context.theory_of ctxt
     fun find_dist t =
       (case t of
         \<^Const_>\<open>dist T for _ _\<close>  => SOME T
       | t1 $ t2 => (case find_dist t1 of NONE => find_dist t2 | some => some)
       | Abs _ => find_dist (#2 (Term.dest_abs_global t))
       | _ => NONE)
     fun find_eq t =
       (case t of
         \<^Const_>\<open>HOL.eq T for l r\<close> =>
           if Sign.of_sort thy (T, \<^sort>\<open>metric_space\<close>) then SOME T
           else (case find_eq l of NONE => find_eq r | some => some)
       | t1 $ t2 => (case find_eq t1 of NONE => find_eq t2 | some => some)
       | Abs _ => find_eq (#2 (Term.dest_abs_global t))
       | _ => NONE)
     in
       (case find_dist tm of
         SOME ty => ty
       | NONE =>
           case find_eq tm of
             SOME ty => ty
           | NONE => error "No Metric Space was found")
     end
 
 (* solve \<exists> by proving the goal for a single witness from the metric space *)
 fun exists_tac ctxt = CSUBGOAL (fn (goal, i) =>
   let
     val _ = \<^assert> (i = 1)
     val metric_ty = guess_metric ctxt (Thm.term_of goal)
     val points = find_points ctxt metric_ty goal
 
     fun try_point_tac ctxt pt =
       let
         val ex_rule =
           \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm pt\<close> and x = pt in
             lemma (schematic) \<open>P x \<Longrightarrow> \<exists>x::'a. P x\<close> by (rule exI)\<close>
       in
         HEADGOAL (resolve_tac ctxt [ex_rule] ORELSE'
         (*variable doesn't occur in body*)
         resolve_tac ctxt @{thms exI}) THEN
         trace_tac ctxt ("Removed existential quantifier, try " ^ @{make_string} pt) THEN
         HEADGOAL (try_points_tac ctxt)
       end
     and try_points_tac ctxt = SUBGOAL (fn (g, _) =>
       if is_exists g then
         FIRST (map (try_point_tac ctxt) points)
       else if is_forall g then
         resolve_tac ctxt @{thms HOL.allI} 1 THEN
         Subgoal.FOCUS (fn {context = ctxt', ...} =>
           trace_tac ctxt "Removed universal quantifier" THEN
           try_points_tac ctxt' 1) ctxt 1
       else basic_metric_arith_tac ctxt metric_ty 1)
   in try_points_tac ctxt 1 end)
 
 fun metric_arith_tac ctxt =
   SELECT_GOAL (
     (*unfold common definitions to get rid of sets*)
     unfold_tac ctxt 1 THEN
     (*remove all meta-level connectives*)
     IF_UNSOLVED (Object_Logic.full_atomize_tac ctxt 1) THEN
     (*convert goal to prenex form*)
     IF_UNSOLVED (prenex_tac ctxt 1) THEN
     (*and NNF to ?*)
     IF_UNSOLVED (nnf_tac ctxt 1) THEN
     (*turn all universally quantified variables into free variables, by focusing the subgoal*)
     REPEAT (HEADGOAL (resolve_tac ctxt @{thms HOL.allI})) THEN
     IF_UNSOLVED (SUBPROOF (fn {context = ctxt', ...} =>
       trace_tac ctxt' "Focused on subgoal" THEN
       exists_tac ctxt' 1) ctxt 1))
 
 end