# HG changeset patch
# User wenzelm
# Date 1635530673 -7200
# Node ID 9264ef3a2ba37fb5be0b5705652186b5520c0cf2
# Parent  cd030003efa872053cb1f1d36e4a2a739fa354e1
clarified antiquotations;

diff -r cd030003efa8 -r 9264ef3a2ba3 src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Fri Oct 29 19:49:11 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Fri Oct 29 20:04:33 2021 +0200
@@ -150,9 +150,11 @@
     val real_abs_dist_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms real_abs_dist})
     val maxdist_thm =
-      @{thm maxdist_thm} |>
-      infer_instantiate' ctxt [SOME fset_ct, SOME x, SOME y] |>
-      solve_prems
+      \<^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 *)
@@ -179,9 +181,11 @@
     val dist_refl_sym_simp =
       Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self})
     val metric_eq_thm =
-      @{thm metric_eq_thm} |>
-      infer_instantiate' ctxt [SOME x, SOME fset_ct, SOME y] |>
-      solve_prems
+      \<^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*)
@@ -190,10 +194,12 @@
   end
 
 (* build list of theorems "0 \<le> dist x y" for all dist terms in ct *)
-fun augment_dist_pos ctxt metric_ty ct =
+fun augment_dist_pos metric_ty ct =
   let fun inst dist_ct =
-    let val (xct, yct) = Thm.dest_binop dist_ct
-    in infer_instantiate' ctxt [SOME xct, SOME yct] @{thm zero_le_dist} end
+    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>) *)
@@ -213,7 +219,7 @@
 (* decision procedure for linear real arithmetic *)
 fun lin_real_arith_tac ctxt metric_ty i goal =
   let
-    val dist_thms = augment_dist_pos ctxt metric_ty (Thm.cprem_of goal 1)
+    val dist_thms = augment_dist_pos metric_ty (Thm.cprem_of goal 1)
     val ctxt' = argo_trace_ctxt ctxt
   in (Argo_Tactic.argo_tac ctxt' dist_thms) i goal end