src/Pure/Isar/proof_context.ML
changeset 6870 43d64c520d11
parent 6852 fe39a3054d82
child 6875 df31250ccb3a
--- 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;