author | traytel |
Fri, 19 Jul 2013 16:36:13 +0200 | |
changeset 52708 | 13e6014ed42b |
parent 52707 | e2d08b9c9047 (diff) |
parent 52706 | 5f86b30badd9 (current diff) |
child 52709 | 0e4bacf21e77 |
--- a/src/Tools/adhoc_overloading.ML Fri Jul 19 15:48:04 2013 +0200 +++ b/src/Tools/adhoc_overloading.ML Fri Jul 19 16:36:13 2013 +0200 @@ -176,7 +176,7 @@ Term_Subst.map_aterms_same (insert_variants_same ctxt t) t) ts ctxt; fun uncheck ts ctxt = - if Config.get ctxt show_variants then NONE + if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then NONE else gen_check_uncheck (insert_overloaded_same ctxt) ts ctxt; fun reject_unresolved ts ctxt =