diff -r 60c134fdd290 -r ee19c92ae8b4 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Dec 10 10:44:56 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Dec 10 13:45:44 2014 +0100
@@ -51,6 +51,7 @@
   val is_document_raw: keywords -> string -> bool
   val is_document: keywords -> string -> bool
   val is_theory_begin: keywords -> string -> bool
+  val is_theory_end: keywords -> string -> bool
   val is_theory_load: keywords -> string -> bool
   val is_theory: keywords -> string -> bool
   val is_theory_body: keywords -> string -> bool
@@ -60,6 +61,8 @@
   val is_proof_goal: keywords -> string -> bool
   val is_qed: keywords -> string -> bool
   val is_qed_global: keywords -> string -> bool
+  val is_proof_asm: keywords -> string -> bool
+  val is_improper: keywords -> string -> bool
   val is_printed: keywords -> string -> bool
 end;
 
@@ -217,6 +220,7 @@
 val is_document = command_category [document_heading, document_body, document_raw];
 
 val is_theory_begin = command_category [thy_begin];
+val is_theory_end = command_category [thy_end];
 
 val is_theory_load = command_category [thy_load];
 
@@ -239,6 +243,9 @@
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
+val is_proof_asm = command_category [prf_asm, prf_asm_goal];
+val is_improper = command_category [qed_script, prf_script, prf_asm_goal_script];
+
 fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
 
 end;