changeset 12680 | 1556a7637439 |
parent 12579 | f4e0ce28aa8e |
child 12702 | 721b622d8967 |
--- 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;