# HG changeset patch # User Kevin Kappelmann # 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)) =