# HG changeset patch
# User wenzelm
# Date 1010580686 -3600
# Node ID 1556a76374394f08a1862d1f2b2bcd3f33f46b07
# Parent  8ed660138f8324713ef182d0df2c7c35edbee036
tuned message;

diff -r 8ed660138f83 -r 1556a7637439 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Jan 09 13:43:05 2002 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Jan 09 13:51:26 2002 +0100
@@ -648,7 +648,7 @@
       | prt_elem (Defines defs) = items "defines" (map prt_def defs)
       | prt_elem (Notes facts) = items "notes" (map prt_fact facts);
   in
-    Pretty.big_list "locale elements:" (map (Pretty.chunks o prt_elem) (flat (map #2 elemss)))
+    Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) (flat (map #2 elemss)))
     |> Pretty.writeln
   end;