diff -r 708c613370ab -r e089757b952a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 29 06:03:41 2004 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 29 06:04:01 2004 +0200
@@ -51,6 +51,7 @@
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val improper_command: string -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
+  val is_keyword: string -> bool
   val dest_keywords: unit -> string list
   val dest_parsers: unit -> (string * string * string * bool) list
   val print_outer_syntax: unit -> unit
@@ -204,6 +205,7 @@
 
 (* print syntax *)
 
+fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
 fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
 
 fun dest_parsers () =