# HG changeset patch
# User wenzelm
# Date 1344092202 -7200
# Node ID 951bc4c3ee173e007b76eea2def8d86e8b760070
# Parent  206144b13849c80e781bd8a012a904de87bc90c4
refined outer syntax;

diff -r 206144b13849 -r 951bc4c3ee17 src/Pure/Isar/outer_syntax.scala
--- 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)
 
diff -r 206144b13849 -r 951bc4c3ee17 src/Pure/System/build.scala
--- 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"))
             }