src/Pure/Isar/keyword.ML

 signature KEYWORD =
 sig
   type T
   val kind_of: T -> string
   val kind_files_of: T -> string * string list
-  val control: T
   val diag: T
   val thy_begin: T
   val thy_end: T
   val thy_heading1: T
   val thy_heading2: T

   val command_files: string -> Path.T -> Path.T list
   val command_tags: string -> string list
   val dest: unit -> string list * string list
   val define: string * T option -> unit
   val is_diag: string -> bool
-  val is_control: string -> bool
-  val is_regular: string -> bool
   val is_heading: string -> bool
   val is_theory_begin: string -> bool
   val is_theory_load: string -> bool
   val is_theory: string -> bool
   val is_theory_body: string -> bool

   Keyword {kind = kind, files = files @ fs, tags = tags};
 
 
 (* kinds *)
 
-val control = kind "control";
 val diag = kind "diag";
 val thy_begin = kind "thy_begin";
 val thy_end = kind "thy_end";
 val thy_heading1 = kind "thy_heading1";
 val thy_heading2 = kind "thy_heading2";

 val prf_asm_goal = kind "prf_asm_goal";
 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,
+  [diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
     thy_load, thy_decl, thy_decl_block, 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];
 
 

         NONE => false
       | SOME k => Symtab.defined tab (kind_of k))
   end;
 
 val is_diag = command_category [diag];
-val is_control = command_category [control];
-val is_regular = not o command_category [diag, control];
 
 val is_heading =
   command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
     prf_heading2, prf_heading3, prf_heading4];