# 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 (\\<^sup>n,dist\<^sub>\) *) -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 (\\<^sup>n,dist\<^sub>\) *) - 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 \\<^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 \\<^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 =