src/Pure/Isar/outer_keyword.scala
changeset 29450 ac7f67be7f1f
parent 29449 6e7745d35a30
child 32450 375db037f4d2
--- 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)
 }