proper p' instead of p (amending 52c7c42e7e27);

proper context for Goal.prove_internal;

discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily; Simplifier and equational conversions demand a proper proof context;