# 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) }