# HG changeset patch
# User wenzelm
# Date 1374061555 -7200
# Node ID 8d749ebd9ab8c2412cbf0c0e12f89b796cb2c051
# Parent  fb028440473e863c129a3b4915ea6abfd3761d17
take context from static theory, not dynamic theory certificate;

diff -r fb028440473e -r 8d749ebd9ab8 src/Tools/induct.ML
--- 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));