src/Pure/Isar/keyword.ML

   val thy_load: T
   val thy_load_files: string list -> T
   val thy_script: T
   val thy_goal: T
   val qed: T
+  val qed_script: T
   val qed_block: T
   val qed_global: T
   val prf_heading2: T
   val prf_heading3: T
   val prf_heading4: T

 val thy_load = kind "thy_load";
 fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
 val thy_script = kind "thy_script";
 val thy_goal = kind "thy_goal";
 val qed = kind "qed";
+val qed_script = kind "qed_script";
 val qed_block = kind "qed_block";
 val qed_global = kind "qed_global";
 val prf_heading2 = kind "prf_heading2";
 val prf_heading3 = kind "prf_heading3";
 val prf_heading4 = kind "prf_heading4";

 val prf_asm_goal_script = kind "prf_asm_goal_script";
 val prf_script = kind "prf_script";
 
 val kinds =
   [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
+    thy_load, thy_decl, thy_script, thy_goal, 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];
 
 
 (* tags *)

 val is_theory = command_category
   [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
     thy_load, thy_decl, thy_script, thy_goal];
 
 val is_proof = command_category
-  [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
+  [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 is_proof_body = command_category
   [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open, prf_close, prf_chain,
     prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_theory_goal = command_category [thy_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
-val is_qed = command_category [qed, qed_block];
+val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
 end;