Auto-indent incorrectly indents comments and overloads if they follow theorems defined using SPEC ``...``

[Eric-C-Hall]

If I have the following code:

open HolKernel Parse boolLib bossLib;

Definition foo_def:
  foo (x : num) = ARB
End

Theorem foo_two = SPEC “2 : num” foo_def;

(* This comment will be auto-indented incorrectly *)

Overload foo_overload = “foo 2”; (* This overload is also auto-indented incorrectly, which makes the code not work, because the overload needs to be unindented. *)

Theorem bar = SPEC “3 : num” foo_def; (* However, this theorem is auto-indented correctly, as will definitions, and "val ..." *)

And I apply auto-indent to it, I get:

open HolKernel Parse boolLib bossLib;

Definition foo_def:
  foo (x : num) = ARB
End

Theorem foo_two = SPEC “2 : num” foo_def;

        (* This comment will be auto-indented incorrectly *)

        Overload foo_overload = “foo 2”; (* This overload is also auto-indented incorrectly, which makes the code not work, because the overload needs to be unindented. *)

Theorem bar = SPEC “3 : num” foo_def; (* However, this theorem is auto-indented correctly, as will definitions, and "val ..." *)

Which is indented incorrectly, and breaks the code because the overload does not work when indented like that