--- 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);