Maybe a guess in the blue, but here is what grep tells me: ~$ grep base_name ~/isabelle/src/HOL/Tools/ -r | grep Quick /Users/traytel/isabelle/src/HOL/Tools//Quickcheck/abstract_generators.ML: val name = Long_Name.base_name tyco
I have not investigated further. Dmitriy > On 27 Feb 2016, at 19:36, Makarius <makar...@sketis.net> wrote: > > 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 > src/HOL/Tools/Quickcheck/random_generators.ML: compile_generator_expr_raw / > iterate_and_collect. It think it is coming from "compile" defined as > Code_Runtime.dynamic_value_strict. > > It is very difficult to figure out where it really happens, due to all these > indirections of Random_Engine.run etc. > > > Makarius > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
