# HG changeset patch
# User wenzelm
# Date 1231706999 -3600
# Node ID ac7f67be7f1fb7288e0a6f0aaf056373f5847a51
# Parent  6e7745d35a3038cf3b3c18da71cb3f289881fd43
tuned categories;

diff -r 6e7745d35a30 -r ac7f67be7f1f src/Pure/Isar/outer_keyword.scala
--- a/src/Pure/Isar/outer_keyword.scala	Sun Jan 11 20:40:09 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.scala	Sun Jan 11 21:49:59 2009 +0100
@@ -35,11 +35,11 @@
   val minor = Set(MINOR)
   val control = Set(CONTROL)
   val diag = Set(DIAG)
-  val theory0 = Set(THY_BEGIN, THY_SWITCH, THY_END)
-  val theory1 = Set(THY_HEADING)
+  val heading = Set(THY_HEADING, PRF_HEADING)
+  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
-  val proof1 = Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK, PRF_OPEN,
-    PRF_CLOSE, PRF_CHAIN, PRF_DECL)
+  val proof1 =
+    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 }