[isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)
makarius at sketis.net
Sat Feb 27 19:36:34 CET 2016
On Sat, 27 Feb 2016, Florian Haftmann wrote:
> Are you still close enough to obtain an ML traceback? It will take some
> time for me to analyze this.
The exception trace (produced with polyml-5.3.0) points to
/ iterate_and_collect. It think it is coming from "compile" defined as
It is very difficult to figure out where it really happens, due to all
these indirections of Random_Engine.run etc.
More information about the isabelle-dev