# HG changeset patch
# User ballarin
# Date 1111678600 -3600
# Node ID 8b40f741597ccada8982bc197f54a1bba922f49a
# Parent  4723248c982b5e073e09b0dec7df730820e2b061
*** empty log message ***

diff -r 4723248c982b -r 8b40f741597c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Mar 24 16:34:15 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Mar 24 16:36:40 2005 +0100
@@ -1501,7 +1501,7 @@
   in (defs_thy, (statement, intro, axioms)) end;
 
 (* CB: modify the locale elements:
-   - assume elements become notes elements,
+   - assumes elements become notes elements,
    - notes elements are lifted
 *)