src/Tools/induct.ML
changeset 52684 8d749ebd9ab8
parent 51717 9e7d1c139569
child 52732 b4da1f2ec73f
     1.1 --- a/src/Tools/induct.ML	Wed Jul 17 11:38:57 2013 +0200
     1.2 +++ b/src/Tools/induct.ML	Wed Jul 17 13:45:55 2013 +0200
     1.3 @@ -162,8 +162,7 @@
     1.4    | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
     1.5  
     1.6  val rearrange_eqs_simproc =
     1.7 -  Simplifier.simproc_global
     1.8 -    (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
     1.9 +  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"]
    1.10      (fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));
    1.11  
    1.12