# HG changeset patch
# User wenzelm
# Date 1215689853 -7200
# Node ID fb07f3b328630d37840fd5d7a92fd4b0a3be3e9a
# Parent  59b54d80d2ae0746e30f6a7fe76f7296d9c1af4f
added is_diag;

diff -r 59b54d80d2ae -r fb07f3b32863 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Thu Jul 10 13:37:31 2008 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Thu Jul 10 13:37:33 2008 +0200
@@ -49,6 +49,7 @@
   val command: string -> T -> unit
   val is_theory: string -> bool
   val is_proof: string -> bool
+  val is_diag: string -> bool
 end;
 
 structure OuterKeyword: OUTER_KEYWORD =
@@ -181,4 +182,6 @@
   (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]);
 
+val is_diag = command_category [kind_of diag];
+
 end;