src/Pure/goal_display.ML
changeset 39115 a00da1674c1c
parent 39050 600de0485859
child 39116 f14735a88886
--- a/src/Pure/goal_display.ML	Fri Sep 03 14:20:47 2010 +0200
+++ b/src/Pure/goal_display.ML	Fri Sep 03 15:54:03 2010 +0200
@@ -63,8 +63,10 @@
 
 in
 
-fun pretty_goals ctxt {total, main, maxgoals} state =
+fun pretty_goals ctxt0 {total, main, maxgoals} state =
   let
+    val ctxt = Config.put show_free_types false ctxt0;
+
     val prt_sort = Syntax.pretty_sort ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
     val prt_term = Syntax.pretty_term ctxt;
@@ -115,9 +117,8 @@
       (if types then pretty_vars prop else []) @
       (if sorts then pretty_varsT prop else []);
   in
-    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))
+    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;