# HG changeset patch
# User wenzelm
# Date 1011125341 -3600
# Node ID bdd17e7b5bd947da055f26aa7329b52085c60028
# Parent  0f70bfe510eea37822d0fe20a55d3b9af93e0371
removed second copy of show_hyps;

diff -r 0f70bfe510ee -r bdd17e7b5bd9 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jan 15 18:51:20 2002 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Jan 15 21:09:01 2002 +0100
@@ -109,7 +109,6 @@
   val get_case: context -> string -> string option list -> RuleCases.T
   val add_cases: (string * RuleCases.T) list -> context -> context
   val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list)
-  val show_hyps: bool ref
   val pretty_term: context -> term -> Pretty.T
   val pretty_typ: context -> typ -> Pretty.T
   val pretty_sort: context -> sort -> Pretty.T
@@ -650,11 +649,9 @@
 
 val string_of_term = Pretty.string_of oo pretty_term;
 
-val show_hyps = ref false;
-
 fun pretty_thm ctxt thm =
-  if ! show_hyps then setmp Display.show_hyps true (fn () =>
-    Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm) ()
+  if ! Display.show_hyps then
+    Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm
   else pretty_term ctxt (#prop (Thm.rep_thm thm));
 
 fun pretty_thms ctxt [th] = pretty_thm ctxt th