[isabelle] Unifier trace in solve_direct

Hi List,

when I type solve_direct, it outputs a lot of unifier trace messages
"Enter MATCH" and "unification bound exceeded". 

I think it is due to some lemma that I have proven, and that hapens to
have an unfortunately shaped conclusion.

How can I identify the lemma? Is there any general method?

If I have identified the lemma, how can I exclude it from solve_direct?

Thanks in advance for any hints,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.