theory Proofs imports Pure begin ML "Proofterm.proofs := 2" end