src/Pure/Isar/proof_context.ML

   val fix_frees: term list -> context -> context
   val bind_skolem: context -> string list -> term -> term
   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
   val pretty_thm: context -> thm -> Pretty.T
   val pretty_thms: context -> thm list -> Pretty.T

 val pretty_typ = Sign.pretty_typ o sign_of;
 val pretty_sort = Sign.pretty_sort o sign_of;
 
 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
   | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));