# HG changeset patch
# User skalberg
# Date 1062358078 -7200
# Node ID 14a12da7288e4760deca73b8674fbfc17945ec20
# Parent  06b19a7e675a70b43abde0d4ca755490b12bf6df
Makes interactive proof scripting recognize the show_all_types flag.

diff -r 06b19a7e675a -r 14a12da7288e src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Aug 31 21:24:29 2003 +0200
+++ b/src/Pure/display.ML	Sun Aug 31 21:27:58 2003 +0200
@@ -338,9 +338,9 @@
       (if sorts then pretty_varsT prop else []);
   in
     setmp show_no_free_types true
-      (setmp show_types (! show_types orelse ! show_sorts)
+      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
         (setmp show_sorts false pretty_gs))
-   (! show_types orelse ! show_sorts, ! show_sorts)
+   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   end;
 
 fun pretty_goals_marker bg n th =