# HG changeset patch
# User wenzelm
# Date 861357672 -7200
# Node ID 395686b418a4e38b7d6356a86b74e300ae24a27e
# Parent  d9f6299dbf9f949f447deac076e2b227a8115173
print_goals: fixed show_sorts semantics;

diff -r d9f6299dbf9f -r 395686b418a4 src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Apr 18 11:58:38 1997 +0200
+++ b/src/Pure/display.ML	Fri Apr 18 12:01:12 1997 +0200
@@ -175,12 +175,17 @@
     val ngoals = length As;
 
     val orig_no_freeTs = ! show_no_free_types;
+    val orig_types = ! show_types;
     val orig_sorts = ! show_sorts;
 
     fun restore () =
-      (show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts);
+      (show_no_free_types := orig_no_freeTs;
+        show_types := orig_types;
+        show_sorts := orig_sorts);
   in
-    (show_no_free_types := true; show_sorts := false;
+    (show_no_free_types := true;
+      show_types := (orig_types orelse orig_sorts);
+      show_sorts := false;
       Pretty.writeln (pretty_term B);
       if ngoals = 0 then writeln "No subgoals!"
       else if ngoals > maxgoals then
@@ -192,7 +197,7 @@
 
       if orig_sorts then
         (print_types prop; print_sorts prop)
-      else if ! show_types then
+      else if orig_types then
         print_types prop
       else ())
     handle exn => (restore (); raise exn);