# HG changeset patch
# User wenzelm
# Date 958989447 -7200
# Node ID 25f2bdc02123cf339f15cb03e3e718784d7b0b18
# Parent  813fabceec00482f87a105273fcc424c26abcbf6
show_consts no longer requires show_types;

diff -r 813fabceec00 -r 25f2bdc02123 doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Mon May 22 11:56:55 2000 +0200
+++ b/doc-src/Ref/introduction.tex	Mon May 22 11:57:27 2000 +0200
@@ -287,12 +287,10 @@
 \item[set \ttindexbold{show_sorts};] makes Isabelle show both types
   and the sorts of type variables, independently of the value of
   \texttt{show_types}.
-
-\item[set \ttindexbold{show_consts};] makes Isabelle show types of
-  constants, provided that showing of types is enabled at all.  This
-  is supported for printing of proof states only.  Note that the
-  output can be enormous as polymorphic constants often occur at
-  several different type instances.
+  
+\item[set \ttindexbold{show_consts};] makes Isabelle show types of constants
+  when printing proof states.  Note that the output can be enormous as
+  polymorphic constants often occur at several different type instances.
 
 \item[set \ttindexbold{long_names};] forces names of all objects
   (types, constants, theorems, etc.) to be printed in their fully
diff -r 813fabceec00 -r 25f2bdc02123 src/Pure/display.ML
--- a/src/Pure/display.ML	Mon May 22 11:56:55 2000 +0200
+++ b/src/Pure/display.ML	Mon May 22 11:57:27 2000 +0200
@@ -228,7 +228,7 @@
   end;
 
 
-(*also show consts in case of showing types?*)
+(*show consts with types in proof state output?*)
 val show_consts = ref false;
 
 
diff -r 813fabceec00 -r 25f2bdc02123 src/Pure/locale.ML
--- a/src/Pure/locale.ML	Mon May 22 11:56:55 2000 +0200
+++ b/src/Pure/locale.ML	Mon May 22 11:57:27 2000 +0200
@@ -639,7 +639,7 @@
               [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
           else pretty_subgoals As) @
         pretty_ffpairs tpairs @
-        (if types andalso ! show_consts then pretty_consts prop else []) @
+        (if ! show_consts then pretty_consts prop else []) @
         (if types then pretty_vars prop else []) @
         (if sorts then pretty_varsT prop else []);
     in