Fix: evaluations within proof terms have to be adapted as well

	modified:   ocaml/proof.ml