# HG changeset patch
# User wenzelm
# Date 1116773477 -7200
# Node ID 070ed43b86f8bd0a3531675959961acfcd4cc136
# Parent  a2c790d145ba7841e978741e615191844edcab92
added ident_with;

diff -r a2c790d145ba -r 070ed43b86f8 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Sun May 22 16:51:16 2005 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Sun May 22 16:51:17 2005 +0200
@@ -19,6 +19,7 @@
   val pos_of: token -> string
   val is_kind: token_kind -> token -> bool
   val keyword_with: (string -> bool) -> token -> bool
+  val ident_with: (string -> bool) -> token -> bool
   val name_of: token -> string
   val is_proper: token -> bool
   val is_semicolon: token -> bool
@@ -110,6 +111,9 @@
 fun keyword_with pred (Token (_, (Keyword, x))) = pred x
   | keyword_with _ _ = false;
 
+fun ident_with pred (Token (_, (Ident, x))) = pred x
+  | ident_with _ _ = false;
+
 fun is_proper (Token (_, (Space, _))) = false
   | is_proper (Token (_, (Comment, _))) = false
   | is_proper _ = true;