tuned msgs;

--- a/src/Pure/Isar/proof_context.ML	Thu Jul 06 18:11:48 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jul 06 18:12:17 2000 +0200
@@ -175,7 +175,7 @@
 (* local theorems *)
 
 fun pretty_thms (Context {thms, ...}) =
-  pretty_items pretty_thm "local theorems:" (mapfilter smash_option (Symtab.dest thms));
+  pretty_items pretty_thm "facts:" (mapfilter smash_option (Symtab.dest thms));
 
 val print_thms = Pretty.writeln o Pretty.chunks o pretty_thms;