src/Pure/goal_display.ML

--- a/src/Pure/goal_display.ML	Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/goal_display.ML	Sat Oct 17 15:57:51 2009 +0200
@@ -108,9 +108,9 @@
       (if types then pretty_vars prop else []) @
       (if sorts then pretty_varsT prop else []);
   in
-    setmp show_no_free_types true
-      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
-        (setmp show_sorts false pretty_gs))
+    setmp_CRITICAL show_no_free_types true
+      (setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
+        (setmp_CRITICAL show_sorts false pretty_gs))
    (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   end;