src/HOL/BNF/Tools/bnf_wrap_tactics.ML

   val mk_case_cong_tac: thm -> thm list -> tactic
   val mk_case_conv_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
     tactic
   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
-  val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
-    thm list list list -> thm list list list -> tactic
+  val mk_expand_tac: int -> int list -> thm -> thm -> thm list -> thm list list list ->
+    thm list list list -> tactic
   val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
   val mk_other_half_disc_exclude_tac: thm -> tactic
   val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic
   val mk_split_asm_tac: Proof.context -> thm -> tactic

       atac
     else
       REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
       SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
 
-fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
-    disc_excludesss' =
+fun mk_expand_tac n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss disc_excludesss' =
   if ms = [0] then
     rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses RS sym))) 1
   else
     let
       val ks = 1 upto n;