--- 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
--- 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;
--- 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