# HG changeset patch
# User traytel
# Date 1384773960 -3600
# Node ID f6ffe53387ef4d849627f47a22cc95d2da49e9e1
# Parent  663a927fdc88e9950f3e58dbd127d46e4a1bbda7
reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798

diff -r 663a927fdc88 -r f6ffe53387ef src/Tools/adhoc_overloading.ML
--- 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