1.1 --- a/src/Pure/Isar/keyword.scala	Fri Mar 16 18:21:22 2012 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Fri Mar 16 20:33:33 2012 +0100
     1.3 @@ -14,27 +14,26 @@
     1.4    val MINOR = "minor"
     1.5    val CONTROL = "control"
     1.6    val DIAG = "diag"
     1.7 -  val THY_BEGIN = "theory-begin"
     1.8 -  val THY_SWITCH = "theory-switch"
     1.9 -  val THY_END = "theory-end"
    1.10 -  val THY_HEADING = "theory-heading"
    1.11 -  val THY_DECL = "theory-decl"
    1.12 -  val THY_SCRIPT = "theory-script"
    1.13 -  val THY_GOAL = "theory-goal"
    1.14 -  val THY_SCHEMATIC_GOAL = "theory-schematic-goal"
    1.15 +  val THY_BEGIN = "thy_begin"
    1.16 +  val THY_END = "thy_end"
    1.17 +  val THY_HEADING = "thy_heading"
    1.18 +  val THY_DECL = "thy_decl"
    1.19 +  val THY_SCRIPT = "thy_script"
    1.20 +  val THY_GOAL = "thy_goal"
    1.21 +  val THY_SCHEMATIC_GOAL = "thy_schematic_goal"
    1.22    val QED = "qed"
    1.23 -  val QED_BLOCK = "qed-block"
    1.24 -  val QED_GLOBAL = "qed-global"
    1.25 -  val PRF_HEADING = "proof-heading"
    1.26 -  val PRF_GOAL = "proof-goal"
    1.27 -  val PRF_BLOCK = "proof-block"
    1.28 -  val PRF_OPEN = "proof-open"
    1.29 -  val PRF_CLOSE = "proof-close"
    1.30 -  val PRF_CHAIN = "proof-chain"
    1.31 -  val PRF_DECL = "proof-decl"
    1.32 -  val PRF_ASM = "proof-asm"
    1.33 -  val PRF_ASM_GOAL = "proof-asm-goal"
    1.34 -  val PRF_SCRIPT = "proof-script"
    1.35 +  val QED_BLOCK = "qed_block"
    1.36 +  val QED_GLOBAL = "qed_global"
    1.37 +  val PRF_HEADING = "prf_heading"
    1.38 +  val PRF_GOAL = "prf_goal"
    1.39 +  val PRF_BLOCK = "prf_block"
    1.40 +  val PRF_OPEN = "prf_open"
    1.41 +  val PRF_CLOSE = "prf_close"
    1.42 +  val PRF_CHAIN = "prf_chain"
    1.43 +  val PRF_DECL = "prf_decl"
    1.44 +  val PRF_ASM = "prf_asm"
    1.45 +  val PRF_ASM_GOAL = "prf_asm_goal"
    1.46 +  val PRF_SCRIPT = "prf_script"
    1.47  
    1.48  
    1.49    /* categories */
    1.50 @@ -43,9 +42,8 @@
    1.51    val control = Set(CONTROL)
    1.52    val diag = Set(DIAG)
    1.53    val theory =
    1.54 -    Set(THY_BEGIN, THY_SWITCH, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT,
    1.55 -      THY_GOAL, THY_SCHEMATIC_GOAL)
    1.56 -  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    1.57 +    Set(THY_BEGIN, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
    1.58 +  val theory1 = Set(THY_BEGIN, THY_END)
    1.59    val theory2 = Set(THY_DECL, THY_GOAL)
    1.60    val proof =
    1.61      Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,