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

[Peter Lammich]

> 
> 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.

--
  Peter



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