diff -r b2d8d50b9efb -r a7774e1e1f1b src/Pure/Tools/adhoc_overloading.ML --- a/src/Pure/Tools/adhoc_overloading.ML Tue Jan 28 13:35:08 2025 +0100 +++ b/src/Pure/Tools/adhoc_overloading.ML Tue Jan 28 13:37:02 2025 +0100 @@ -202,7 +202,7 @@ else map (fn t => Term.map_aterms (insert_variants ctxt t) t); fun uncheck ctxt ts = - if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts + if Config.get ctxt show_variants orelse exists (not o can Term.type_of) ts then ts else map (insert_overloaded ctxt) ts; fun reject_unresolved ctxt =