On Wed, 9 Sep 2015, Andreas Lochbihler wrote: > I've committed some changes in 78ece168f5b5 such that most of the > examples work again. Only Hotel_Example_Small_Generator remains > completely broken. Great -- this is a clear move forward, and only one obscure FIXME remaining in src/HOL/ROOT. Makarius