Emacs hangs when using mark tactic twice or inside a term

[Luceat]

Hi,

Using mark tactic (M-h t) twice in a row hangs emacs, recoverable by (C-g g).

Using mark tactic inside a term, such as when the cursor is on h in Cases on 'h' similarily hangs emacs.

[thtuerk]

I played around with this a bit. I can confirm this behavior, but only at the end of a file. If the tactic is followed by "THEN", ">>", "val" and probably some other keywords as well, it seems to work fine.

[Luceat]

For me, this happens also in declarations such as:

val MY_THM = prove( 'goal', (* Buggy behaviour here *) );