src/HOL/Analysis/metric_arith.ML

     (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 i goal =
-  let
-    val dist_thms = augment_dist_pos metric_ty (Thm.cprem_of goal 1)
+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 goal end
+  in Argo_Tactic.argo_tac ctxt' dist_thms i end)
 
 fun basic_metric_arith_tac ctxt metric_ty =
   HEADGOAL (dist_refl_sym_tac ctxt THEN'
   IF_UNSOLVED o (embedding_tac ctxt metric_ty) THEN'
   IF_UNSOLVED o (pre_arith_tac ctxt) THEN'