HIDE X HIDE Y works but HIDE X, Y doesn't

[cpacejo]

This module:

---- MODULE tlapmhidebug ----

AXIOM X == TRUE
AXIOM Y == TRUE

USE X, Y
HIDE X, Y

====

results in the backtrace:

$ tlapm tlapmhidebug.tla 
File "./tlapmhidebug.tla", line 7, character 9:
Error: This expression does not appear in the context and cannot be hidden.

 tlapm ending abnormally with Failure("proof.Gen.set_expr")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from P_gen.gen_step in file "p_gen.ml", line 321, characters 17-62
Called from P_gen.mutate_one in file "p_gen.ml", line 366, characters 8-80
Called from P_gen.mutate in file "p_gen.ml", line 381, characters 35-100
Called from P_gen.mutate in file "p_gen.ml", line 384, characters 24-85
Called from M_gen.generate.visit in file "m_gen.ml", line 84, characters 30-70
Called from M_gen.generate.visit in file "m_gen.ml", line 86, characters 22-34
Called from M_gen.generate.visit in file "m_gen.ml", line 91, characters 22-34
Called from M_gen.generate.visit in file "m_gen.ml", line 91, characters 22-34
Called from M_gen.generate in file "m_gen.ml", line 94, characters 13-33
Called from M_elab.normalize in file "m_elab.ml", line 1293, characters 29-51
Called from Tlapm.process_module in file "tlapm.ml", line 311, characters 29-68
Called from Tlapm.main.f in file "tlapm.ml", line 545, characters 23-43
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 548, characters 13-40
Called from Tlapm.init in file "tlapm.ml", line 560, characters 8-33

but this module:

---- MODULE tlapmhidebug ----

AXIOM X == TRUE
AXIOM Y == TRUE

USE X, Y
HIDE X
HIDE Y

====

works as expected:

$ tlapm tlapmhidebug.tla 
(* created new ".tlacache/tlapmhidebug.tlaps/tlapmhidebug.thy" *)
(* fingerprints written in ".tlacache/tlapmhidebug.tlaps/fingerprints" *)
File "./tlapmhidebug.tla", line 1, character 1 to line 10, character 4:
[INFO]: All 2 obligations proved.

Using latest tlapm 1.5.0, tag 202201050543.

[ahelwer]

Testing shows this check fails at the semantic level, not the syntax level.