src/Pure/Isar/outer_keyword.ML

   val command_keyword: string -> T option
   val command_tags: string -> string list
   val report: unit -> unit
   val keyword: string -> unit
   val command: string -> T -> unit
-  datatype category = Theory | Proof | Other
-  val category_of: string -> category
+  val is_theory: string -> bool
+  val is_proof: string -> bool
 end;
 
 structure OuterKeyword: OUTER_KEYWORD =
 struct
 

 val prf_script = kind "proof-script";
 
 val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
   thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
   prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of;
-
-val thy_kinds =
-  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal] |> map kind_of;
-
-val prf_kinds =
-  [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of;
 
 
 (* tags *)
 
 fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;

   Pretty.writeln (report_command (name, kind)));
 
 
 (* overall category *)
 
-datatype category = Theory | Proof | Other;
+fun command_category ks name =
+  (case command_keyword name of
+    NONE => false
+  | SOME k => member (op =) ks (kind_of k));
 
-fun category_of name =
-  (case command_keyword name of
-    SOME kind =>
-      let val k = kind_of kind in
-        if member (op =) thy_kinds k then Theory
-        else if member (op =) prf_kinds k then Proof
-        else Other
-      end
-  | NONE => error ("Unknown command " ^ quote name));
+val is_theory = command_category
+  (map kind_of [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal]);
+
+val is_proof = command_category
+  (map kind_of [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]);
 
 end;