Fixed short name on wrong token;

isabelle-prover · Nov 21, 2022 · fea631b · fea631b
1 parent 95abe99
commit fea631b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/linter_base/src/lints.scala b/linter_base/src/lints.scala
@@ -647,7 +647,7 @@ object Short_Name extends Parser_Lint
 
   override def parser(report: Reporter): Parser[Some[Lint_Result]] =
     p_command("fun", "primrec", "abbreviation", "definition", "inductive", "inductive_set") ~>
-      elem("ident", _.info.content.length < 2) ^^ {
+      elem("ident", t => t.info.is_ident && t.info.content.length < 2) ^^ {
         case Text.Info(range, token) =>
           report(s"""Name "${token.content}" is too short.""", range, None)
       }