On Tue, 12 Jan 2016, Manuel Eberl wrote: > I commented out the code equation in question and HOL-Codegenerator_Test runs > through again. Thanks. For the historical record: that is Isabelle/18a217591310. (Mercurial changeset ids allow to talk about history in a timeless and stateless manner.) Makarius