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

[Peter Lammich]

Hi List,

I have a tactic that has a debug-mode. In debug-mode, 
it shall output unification trace for certain (but not all) rule
applications.

How to write a tactic 
  resolve_with_tracing: thm list -> int -> tactic

that behaves like resolve_tac, but outputs unification trace?

Best,
  Peter


p.s.
Not sure whether this belongs to user or devel, but the reason 
for my message is  

http://sourceforge.net/p/afp/code/ci/7189f7ffd73e17c2395eb552c89004f5b8e0453e/ 

which seems to be related to tty-mode elimination that is currently
going on in dev-version.