Makes interactive proof scripting recognize the show_all_types flag.
authorskalberg
Sun Aug 31 21:27:58 2003 +0200 (2003-08-31)
changeset 1417814a12da7288e
parent 14177 06b19a7e675a
child 14179 04f905c13502
Makes interactive proof scripting recognize the show_all_types flag.
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sun Aug 31 21:24:29 2003 +0200
     1.2 +++ b/src/Pure/display.ML	Sun Aug 31 21:27:58 2003 +0200
     1.3 @@ -338,9 +338,9 @@
     1.4        (if sorts then pretty_varsT prop else []);
     1.5    in
     1.6      setmp show_no_free_types true
     1.7 -      (setmp show_types (! show_types orelse ! show_sorts)
     1.8 +      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
     1.9          (setmp show_sorts false pretty_gs))
    1.10 -   (! show_types orelse ! show_sorts, ! show_sorts)
    1.11 +   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
    1.12    end;
    1.13  
    1.14  fun pretty_goals_marker bg n th =