replaced datatype category constructivism by is_theory/is_proof;

--- a/src/Pure/Isar/outer_keyword.ML	Wed Jul 02 16:40:17 2008 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Wed Jul 02 16:40:18 2008 +0200
@@ -47,8 +47,8 @@
   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 =
@@ -91,13 +91,6 @@
   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 *)
 
@@ -176,16 +169,16 @@
 
 (* overall category *)
 
-datatype category = Theory | Proof | Other;
-
-fun category_of name =
+fun command_category ks 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));
+    NONE => false
+  | SOME k => member (op =) ks (kind_of k));
+
+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;