setmp Display.show_hyps false;
authorwenzelm
Thu, 01 Jul 1999 17:38:44 +0200
changeset 6870 43d64c520d11
parent 6869 850812ed9976
child 6871 01866edde713
setmp Display.show_hyps false;
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;