exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset basic_gen_simp_tac now takes a looper as _explicit_ argument removed superfluous argument of solve_all_tac corrected safe_asm_full_simp_tac: now also with mutual simplification of prems

re-added refl in safe_solver

removed warn_theory_style;