src/Pure/Isar/token.ML
changeset 68730 0bc491938780
parent 68729 3a02b424d5fb
child 69851 29a4f633609e
     1.1 --- a/src/Pure/Isar/token.ML	Tue Jul 31 21:11:24 2018 +0200
     1.2 +++ b/src/Pure/Isar/token.ML	Tue Jul 31 21:21:20 2018 +0200
     1.3 @@ -43,7 +43,6 @@
     1.4    val is_command_modifier: T -> bool
     1.5    val ident_with: (string -> bool) -> T -> bool
     1.6    val is_proper: T -> bool
     1.7 -  val is_improper: T -> bool
     1.8    val is_comment: T -> bool
     1.9    val is_informal_comment: T -> bool
    1.10    val is_formal_comment: T -> bool
    1.11 @@ -236,8 +235,6 @@
    1.12    | is_proper (Token (_, (Comment _, _), _)) = false
    1.13    | is_proper _ = true;
    1.14  
    1.15 -val is_improper = not o is_proper;
    1.16 -
    1.17  fun is_comment (Token (_, (Comment _, _), _)) = true
    1.18    | is_comment _ = false;
    1.19