# HG changeset patch
# User wenzelm
# Date 1634649631 -7200
# Node ID 54055f568d763acf1be0862f7d98e5e7a0e33c8f
# Parent  6df92c38706394e21600a91f7bfd50d8872d890d
proper tactic combinator;

diff -r 6df92c387063 -r 54055f568d76 src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Tue Oct 19 15:03:00 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Tue Oct 19 15:20:31 2021 +0200
@@ -223,19 +223,18 @@
   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 i goal =
+fun embedding_tac ctxt metric_ty = CSUBGOAL (fn (goal, i) =>
   let
-    val ct = (Thm.cprem_of goal 1)
-    val points = find_points ctxt metric_ty ct
+    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 ct)
+    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 ct)
+    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 goal
-  end
+      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 =