# HG changeset patch
# User wenzelm
# Date 962899937 -7200
# Node ID 21c302a2fd9a6c21ddd5aeefff014ac0a023e9ee
# Parent  798673f65f024cfadb2f61fe3f05a67b082605f9
tuned msgs;

diff -r 798673f65f02 -r 21c302a2fd9a src/Pure/Isar/proof_context.ML
--- 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;