Unsilence deprecation warning regarding list lemmas.
Passed
Robbert Krebbers
created pipeline for commit
2db35c48
, finished
Related merge request !574 to merge robbert/deprecate_rev_length
8 minutes 37 seconds, queued for 3 seconds