[isabelle-dev] How to activate/de-activate unifier-trace from ML-level

Peter Lammich lammich at in.tum.de
Mon Nov 3 11:27:17 CET 2014

> You can contribute indirectly to important reforms that are in the 
> pipeline for a long time by keeping your sources in a more up-to-date 
> state.

As you said, there seems to be no other way of achieving what I
required. I realized that, added a comment (*Argh!*) expressing my
disgust about it, but at the end had to implement the hack in order to
get the desired behaviour.

Now you just removed the desired behaviour, not having a solution how to
get it back ... fortunately, in this particular case, it is not
essential, as this thing was inside some rarely used debugging tool.


>  	Makarius
> ----------------------------------------------------------------------------
>                    http://stop-ttip.org  777,443 people so far
> ----------------------------------------------------------------------------

More information about the isabelle-dev mailing list