[isabelle] ML stack trace?



hi,
i would like to find out more information when the isabelle gives "empty
result sequence".
it seems this exception is raised by a line proof_history.ML, so i tried to
use polyml
debugger to set a breakpoint, recompile the source adding
Poly.Compiler.debug := true
then in proof general use "ML {* open PolyML.Debug; breakAt
(proof_history.ML 70); *}"
but it doesnt seem to work. is there a way to get the stack trace?
thanks
tao




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