refined outer syntax;

--- a/src/Pure/Isar/outer_syntax.scala	Fri Aug 03 19:08:15 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Aug 04 16:56:42 2012 +0200
@@ -49,7 +49,7 @@
     (for ((name, kind) <- keywords) yield {
       if (kind == Keyword.MINOR) quote(name)
       else quote(name) + " :: " + quote(kind)
-    }).toList.sorted.mkString("Outer_Syntax(keywords ", " and ", ")")
+    }).toList.sorted.mkString("keywords\n  ", " and\n  ", "")
 
   def keyword_kind(name: String): Option[String] = keywords.get(name)
 

--- a/src/Pure/System/build.scala	Fri Aug 03 19:08:15 2012 +0200
+++ b/src/Pure/System/build.scala	Sat Aug 04 16:56:42 2012 +0200
@@ -285,6 +285,7 @@
                 (Set.empty[String],
                   Outer_Syntax.init() +
                     // FIXME avoid hardwired stuff!?
+                    ("theory", Keyword.THY_BEGIN) +
                     ("hence", Keyword.PRF_ASM_GOAL, "then have") +
                     ("thus", Keyword.PRF_ASM_GOAL, "then show"))
             }