# HG changeset patch
# User Lukas Stevens <mail@lukas-stevens.de>
# Date 1698957304 -3600
# Node ID 5de1c19ccd92aa0b2c2823eea82e0c1dd8cd6b6b
# Parent  c1bd24ca22b6e4e8708384220e9cae884b839806
clarified;

diff -r c1bd24ca22b6 -r 5de1c19ccd92 src/Tools/induction.ML
--- a/src/Tools/induction.ML	Thu Nov 02 14:10:16 2023 +0000
+++ b/src/Tools/induction.ML	Thu Nov 02 21:35:04 2023 +0100
@@ -46,8 +46,9 @@
             (take n cases ~~ take n hnamess);
       in ((cases', consumes), th) end);
 
-fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
-  NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
+fun induction_tac ctxt simp def_insts arbitrary taking opt_rule facts i =
+  induction_context_tactic simp def_insts arbitrary taking opt_rule facts i
+  |> NO_CONTEXT_TACTIC ctxt;
 
 val _ =
   Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic);