diff -r d44c87988a24 -r 330eb65c9469 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Nov 28 20:36:45 2010 +0100
+++ b/src/Pure/Isar/parse.ML	Sun Nov 28 21:07:28 2010 +0100
@@ -63,6 +63,7 @@
   val xname: xstring parser
   val text: string parser
   val path: Path.T parser
+  val liberal_name: xstring parser
   val parname: string parser
   val parbinding: binding parser
   val sort: string parser
@@ -234,6 +235,8 @@
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 val path = group "file name/path specification" name >> Path.explode;
 
+val liberal_name = keyword_ident_or_symbolic || xname;
+
 val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
 val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;