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

[Makarius]

On Tue, 4 Nov 2014, Makarius wrote:

> Strange hacks that work around the absence of proper options encumber 
> the introduction of them eventually.  It is the usual bootstrap problem 
> for reforms.
>
> I actually did start some work in the vicinity of resolve_tac with 
> proper context recently, but it will require more time to revisit really 
> ancient parts of the system, not to say ancient habits.

Here is an update on this pending thread: current Isabelle/50b60f501b05 is 
the main move to proper context for resolve_tac etc.  After endless years 
of preparation to "localize" the majority of Isabelle tools, it turned out 
a releatively small change.

What remains are slightly odd entry points without context: 
resolve0_tac/rtac, eresolve_tac/etac, dresolve_tac/dtac.  We could 
probably remove them altogether, but there are a lot of remaining uses in 
the new datatype implementation, which I don't want to change myself.


 	Makarius