# HG changeset patch # User wenzelm # Date 1385153870 -3600 # Node ID bf2519f2bd01514a80fb1610240097c43615a158 # Parent 50169ef2cca300893622e660fb5a23399b9af9b1 reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798 (clone of f6ffe53387ef); diff -r 50169ef2cca3 -r bf2519f2bd01 src/Tools/adhoc_overloading.ML --- a/src/Tools/adhoc_overloading.ML Thu Nov 21 22:13:11 2013 +0100 +++ b/src/Tools/adhoc_overloading.ML Fri Nov 22 21:57:50 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