# HG changeset patch
# User wenzelm
# Date 930843524 -7200
# Node ID 43d64c520d1139ad548d505704e651870bbb22ad
# Parent  850812ed9976755e531204597d413bd9148a84e8
setmp Display.show_hyps false;

diff -r 850812ed9976 -r 43d64c520d11 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jul 01 17:24:29 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jul 01 17:38:44 1999 +0200
@@ -141,7 +141,8 @@
 (* local theorems *)
 
 fun strings_of_thms (Context {thms, ...}) =
-  strings_of_items Display.pretty_thm "Local theorems:" (Symtab.dest thms);
+  strings_of_items (setmp Display.show_hyps false Display.pretty_thm)
+    "Local theorems:" (Symtab.dest thms);
 
 val print_thms = seq writeln o strings_of_thms;