src/Tools/induct.ML
changeset 52684 8d749ebd9ab8
parent 51717 9e7d1c139569
child 52732 b4da1f2ec73f
--- 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));