src/Tools/adhoc_overloading.ML

   end;
 
 fun check ctxt =
   map (fn t => Term.map_aterms (insert_variants ctxt t) t);
 
-fun uncheck ctxt =
-  if Config.get ctxt show_variants then I
-  else map (insert_overloaded ctxt);
+fun uncheck ctxt ts =
+  if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts
+  else map (insert_overloaded ctxt) ts;
 
 fun reject_unresolved ctxt =
   let
     val the_candidates = the o get_candidates ctxt;
     fun check_unresolved t =