more operations "without_context", assuming that the thm has been properly transferred already;