# HG changeset patch
# User wenzelm
# Date 1519394850 -3600
# Node ID 23d46836a5acfc1390a2502ec20af0df10a73a76
# Parent  8c4806fe827f8317ea76a84913c353a41c680bf3
tuned;

diff -r 8c4806fe827f -r 23d46836a5ac src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Feb 23 14:32:59 2018 +0100
+++ b/src/Pure/Syntax/printer.ML	Fri Feb 23 15:07:30 2018 +0100
@@ -75,7 +75,7 @@
 fun type_emphasis ctxt T =
   T <> dummyT andalso
     (Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
-      Config.get ctxt show_type_emphasis andalso not (can dest_Type T));
+      Config.get ctxt show_type_emphasis andalso not (is_Type T));