src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML

   let val r = length kks in
     HEADGOAL (EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt,
       REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN
     EVERY [REPEAT_DETERM_N r
         (HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
-      if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, HEADGOAL atac,
+      if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac,
       mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs]
   end;
 
 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_maps pre_set_defss =
   let val n = Integer.sum ns in