added theory_to_theory_to_proof, which may change theory before entering the proof; added forget_proof (from isar_thy.ML);