src/Pure/Isar/token.ML
changeset 51266 3007d0bc9cb1
parent 50239 fb579401dc26
child 54519 5fed81762406
--- a/src/Pure/Isar/token.ML	Sun Feb 24 13:46:14 2013 +1100
+++ b/src/Pure/Isar/token.ML	Sun Feb 24 14:11:51 2013 +0100
@@ -32,6 +32,7 @@
   val is_command: T -> bool
   val is_name: T -> bool
   val is_proper: T -> bool
+  val is_improper: T -> bool
   val is_semicolon: T -> bool
   val is_comment: T -> bool
   val is_begin_ignore: T -> bool
@@ -172,6 +173,8 @@
   | is_proper (Token (_, (Comment, _), _)) = false
   | is_proper _ = true;
 
+val is_improper = not o is_proper;
+
 fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
   | is_semicolon _ = false;