# HG changeset patch
# User wenzelm
# Date 1635531359 -7200
# Node ID 779ae499ca8b78071df0bb5a5ecdbe68d08103f4
# Parent  9264ef3a2ba37fb5be0b5705652186b5520c0cf2
proper subgoal addressing;

diff -r 9264ef3a2ba3 -r 779ae499ca8b src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Fri Oct 29 20:04:33 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Fri Oct 29 20:15:59 2021 +0200
@@ -217,11 +217,11 @@
   end)
 
 (* decision procedure for linear real arithmetic *)
-fun lin_real_arith_tac ctxt metric_ty i goal =
+fun lin_real_arith_tac ctxt metric_ty = CSUBGOAL (fn (goal, i) =>
   let
-    val dist_thms = augment_dist_pos metric_ty (Thm.cprem_of goal 1)
+    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'