diff -r 0ee3563803c9 -r 58bedbc18915 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 05 21:59:21 2014 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 05 22:17:05 2014 +0100
@@ -228,30 +228,30 @@
       val session_name = atom("session name", _.is_name)
 
       val option =
-        name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
-      val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
+        name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
+      val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
       val theories =
-        (keyword(GLOBAL_THEORIES) | keyword(THEORIES)) ~!
+        ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
           ((options | success(Nil)) ~ rep(theory_xname)) ^^
           { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
 
       val document_files =
-        keyword(DOCUMENT_FILES) ~!
-          ((keyword("(") ~! (keyword(IN) ~! (path ~ keyword(")"))) ^^
+        $$$(DOCUMENT_FILES) ~!
+          (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
               { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
             rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
 
       command(SESSION) ~!
         (session_name ~
-          ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
-          ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
-          (keyword("=") ~!
-            (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
-              ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
-              ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
+          (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
+          (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
+          ($$$("=") ~!
+            (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
+              (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
+              (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep1(theories) ~
-              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
+              (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
               (rep(document_files) ^^ (x => x.flatten))))) ^^
         { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }