# HG changeset patch
# User traytel
# Date 1374238305 -7200
# Node ID e2d08b9c90471b806899465374315e956e264b30
# Parent  c12602c1b13b0ee6d57a74bcc8ef40583b460c56
permissive uncheck -- allow printing of malformed terms (e.g. in error messages);

diff -r c12602c1b13b -r e2d08b9c9047 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Fri Jul 19 12:00:31 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Fri Jul 19 14:51:45 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 =