# HG changeset patch
# User wenzelm
# Date 931811357 -7200
# Node ID 2af6405a6ef35624d8d2c888983b4dbbedc39eab
# Parent  26d43e26ea61af179de07aa7cd5c21dba635fef0
added show_hyps flag;

diff -r 26d43e26ea61 -r 2af6405a6ef3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jul 12 22:28:56 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jul 12 22:29:17 1999 +0200
@@ -11,6 +11,8 @@
   exception CONTEXT of string * context
   val theory_of: context -> theory
   val sign_of: context -> Sign.sg
+  val show_hyps: bool ref
+  val pretty_thm: thm -> Pretty.T
   val verbose: bool ref
   val print_binds: context -> unit
   val print_thms: context -> unit
@@ -108,6 +110,9 @@
 
 (** print context information **)
 
+val show_hyps = ref false;
+fun pretty_thm th = setmp Display.show_hyps (! show_hyps) Display.pretty_thm th;
+
 val verbose = ref false;
 fun verb f x = if ! verbose then f x else [];
 val verb_string = verb (Library.single o Pretty.string_of);
@@ -145,7 +150,7 @@
 (* local theorems *)
 
 fun strings_of_thms (Context {thms, ...}) =
-  strings_of_items Display.pretty_thm_no_hyps "Local theorems:" (Symtab.dest thms);
+  strings_of_items pretty_thm "Local theorems:" (Symtab.dest thms);
 
 val print_thms = seq writeln o strings_of_thms;