src/Pure/Isar/outer_parse.ML

--- a/src/Pure/Isar/outer_parse.ML	Fri Apr 02 12:25:48 2004 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Fri Apr 02 14:08:30 2004 +0200
@@ -174,7 +174,8 @@
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 
 val uname = underscore >> K None || name >> Some;
-
+  (* CB: underscore yields None, any other name Some with that string.
+     Used, for example, in the renaming of locale parameters.  *)
 
 (* sorts and arities *)