src/Pure/Isar/keyword.scala

   val THY_DECL = "thy_decl"
   val THY_LOAD = "thy_load"
   val THY_SCRIPT = "thy_script"
   val THY_GOAL = "thy_goal"
   val QED = "qed"
+  val QED_SCRIPT = "qed_script"
   val QED_BLOCK = "qed_block"
   val QED_GLOBAL = "qed_global"
   val PRF_HEADING2 = "prf_heading2"
   val PRF_HEADING3 = "prf_heading3"
   val PRF_HEADING4 = "prf_heading4"

     Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
       THY_DECL, THY_SCRIPT, THY_GOAL)
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof =
-    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK,
-      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
+      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
+      PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   val proof1 =
-    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
+    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 improper = Set(THY_SCRIPT, PRF_SCRIPT)
 }