src/Pure/Isar/keyword.scala
changeset 57837 63e3c45b85e1
parent 57836 7944e2588d1c
child 58800 bfed1c26caed
--- 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,