A note in the section on administrative instructions describes the reduction rule for labels as:
label_n {instr^n} val* end -> val^n
However, in the actual section for exiting instr*s, the reduction rule is written as:
label_n {instr*} val^m end -> val^m
For my own sanity, I hope the latter is correct.