# HG changeset patch
# User wenzelm
# Date 1635529751 -7200
# Node ID cd030003efa872053cb1f1d36e4a2a739fa354e1
# Parent  c690435c47ee4dc30ef10d34e7f001693451548e
recursive find_eq, not find_dist;

diff -r c690435c47ee -r cd030003efa8 src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Fri Oct 29 19:43:32 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Fri Oct 29 19:49:11 2021 +0200
@@ -238,7 +238,7 @@
       (case t of
         \<^Const_>\<open>HOL.eq T for l r\<close> =>
           if Sign.of_sort thy (T, \<^sort>\<open>metric_space\<close>) then SOME T
-          else (case find_eq l of NONE => find_dist r (* FIXME find_eq!? *) | some => some)
+          else (case find_eq l of NONE => find_eq r | some => some)
       | t1 $ t2 => (case find_eq t1 of NONE => find_eq t2 | some => some)
       | Abs _ => find_eq (#2 (Term.dest_abs_global t))
       | _ => NONE)