src/HOL/Tools/BNF/bnf_comp.ML

     val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
 
     val wits = map (fn t => fold absfree (Term.add_frees t []) t)
       (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
 
-    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
+    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs))
         Binding.empty Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in

     val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
-    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
+    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
         Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in

     val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
-    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
+    fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
         Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in

     val bnf_wits = map (fn (I, t) =>
         fold Term.absdummy (map (nth As) I)
           (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
       (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
-    fun wit_tac ctxt = ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN
-      mk_simple_wit_tac (wit_thms_of_bnf bnf);
+    fun wit_tac ctxt =
+      ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN
+      mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
       bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
         Binding.empty Binding.empty []
         ((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;