reset show_hyps by default (in accordance to existing Isar practice);

--- a/doc-src/Ref/introduction.tex	Mon Jan 21 16:28:22 2002 +0100
+++ b/doc-src/Ref/introduction.tex	Mon Jan 21 17:02:52 2002 +0100
@@ -252,7 +252,7 @@
 \index{meta-assumptions!printing of}
 \index{types!printing of}\index{sorts!printing of}
 \begin{ttbox} 
-show_hyps     : bool ref \hfill{\bf initially true}
+show_hyps     : bool ref \hfill{\bf initially false}
 show_tags     : bool ref \hfill{\bf initially false}
 show_brackets : bool ref \hfill{\bf initially false}
 show_types    : bool ref \hfill{\bf initially false}

--- a/src/Pure/display.ML	Mon Jan 21 16:28:22 2002 +0100
+++ b/src/Pure/display.ML	Mon Jan 21 17:02:52 2002 +0100
@@ -60,7 +60,7 @@
 (** print thm **)
 
 val goals_limit = ref 10;       (*max number of goals to print -- set by user*)
-val show_hyps = ref true;       (*false: print meta-hypotheses as dots*)
+val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
 val show_tags = ref false;      (*false: suppress tags*)
 
 fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);