# HG changeset patch
# User Kevin Kappelmann <kevin.kappelmann@tum.de>
# Date 1713359067 -7200
# Node ID 39f9084a9668d8e4238f28fb2fabef91801cf741
# Parent  b73df63e0f52615a8d0dc0480dc11e3e7d193775
make adhoc_overloading respect type constraints

diff -r b73df63e0f52 -r 39f9084a9668 src/HOL/Library/adhoc_overloading.ML
--- a/src/HOL/Library/adhoc_overloading.ML	Tue Apr 16 17:28:58 2024 +0200
+++ b/src/HOL/Library/adhoc_overloading.ML	Wed Apr 17 15:04:27 2024 +0200
@@ -154,7 +154,9 @@
 fun get_candidates ctxt (c, T) =
   get_variants ctxt c
   |> Option.map (map_filter (fn (t, T') =>
-    if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t
+    if unifiable_with (Proof_Context.theory_of ctxt) T T'
+    (*keep the type constraint for the type-inference check phase*)
+    then SOME (Type.constraint T t)
     else NONE));
 
 fun insert_variants ctxt t (oconst as Const (c, T)) =