# HG changeset patch
# User wenzelm
# Date 1738068160 -3600
# Node ID 04c704a6b193b7013a8ed79d0010587349123c21
# Parent  a7774e1e1f1b01e28102125bfd8ad8ce7b2f144d
minor performance tuning;

diff -r a7774e1e1f1b -r 04c704a6b193 src/Pure/Tools/adhoc_overloading.ML
--- a/src/Pure/Tools/adhoc_overloading.ML	Tue Jan 28 13:37:02 2025 +0100
+++ b/src/Pure/Tools/adhoc_overloading.ML	Tue Jan 28 13:42:40 2025 +0100
@@ -168,12 +168,13 @@
 
 val the_candidates = the oo get_candidates;
 
-fun insert_variants ctxt t (oconst as Const (c, T)) =
-      (case get_candidates ctxt (c, T) of
-        SOME [] => err_unresolved_overloading ctxt (c, T) t []
+fun insert_variants_same ctxt t : term Same.operation =
+  (fn Const const =>
+      (case get_candidates ctxt const of
+        SOME [] => err_unresolved_overloading ctxt const t []
       | SOME [variant] => variant
-      | _ => oconst)
-  | insert_variants _ _ oconst = oconst;
+      | _ => raise Same.SAME)
+    | _ => raise Same.SAME);
 
 fun insert_overloaded ctxt =
   let
@@ -199,7 +200,7 @@
 
 fun check ctxt =
   if no_variants (Context.Proof ctxt) then I
-  else map (fn t => Term.map_aterms (insert_variants ctxt t) t);
+  else map (fn t => Term.map_aterms (insert_variants_same ctxt t) t);
 
 fun uncheck ctxt ts =
   if Config.get ctxt show_variants orelse exists (not o can Term.type_of) ts then ts