src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Sat Apr 04 14:04:11 2015 +0200
+++ b/src/Pure/Isar/token.ML	Sat Apr 04 21:21:40 2015 +0200
@@ -43,10 +43,11 @@
   val stopper: T Scan.stopper
   val kind_of: T -> kind
   val is_kind: kind -> T -> bool
-  val keyword_with: (string -> bool) -> T -> bool
-  val ident_with: (string -> bool) -> T -> bool
   val is_command: T -> bool
   val is_name: T -> bool
+  val keyword_with: (string -> bool) -> T -> bool
+  val is_private: T -> bool
+  val ident_with: (string -> bool) -> T -> bool
   val is_proper: T -> bool
   val is_improper: T -> bool
   val is_comment: T -> bool
@@ -246,6 +247,8 @@
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   | keyword_with _ _ = false;
 
+val is_private = keyword_with (fn x => x = "private");
+
 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   | ident_with _ _ = false;