more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy;