--- a/src/Tools/adhoc_overloading.ML Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Tools/adhoc_overloading.ML Mon Nov 18 12:26:00 2013 +0100
@@ -178,9 +178,9 @@
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