author | wenzelm |
Wed, 17 Jul 2013 13:45:55 +0200 | |
changeset 52684 | 8d749ebd9ab8 |
parent 52683 | fb028440473e |
child 52685 | 554d684d8520 |
--- a/src/Tools/induct.ML Wed Jul 17 11:38:57 2013 +0200 +++ b/src/Tools/induct.ML Wed Jul 17 13:45:55 2013 +0200 @@ -162,8 +162,7 @@ | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); val rearrange_eqs_simproc = - Simplifier.simproc_global - (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"] + Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"] (fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));