# HG changeset patch # User wenzelm # Date 1406918603 -7200 # Node ID 63e3c45b85e11be462911e3eb54808ff5692e33b # Parent 7944e2588d1ccdb4b96d63cdd30c2251e9f8364e removed unused stuff; diff -r 7944e2588d1c -r 63e3c45b85e1 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Fri Aug 01 20:20:17 2014 +0200 +++ b/src/Pure/Isar/keyword.scala Fri Aug 01 20:43:23 2014 +0200 @@ -53,8 +53,7 @@ val theory = Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL) - val theory1 = Set(THY_BEGIN, THY_END) - val theory2 = Set(THY_DECL, THY_GOAL) + val theory_body = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL) @@ -62,10 +61,6 @@ Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) - val proof1 = - Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, - PRF_CHAIN, PRF_DECL) - val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT) val proof_body = Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN,