src/HOL/BNF/Tools/bnf_comp_tactics.ML

   REPEAT_DETERM (
     atac 1 ORELSE
     REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
     (TRY o dresolve_tac Gwit_thms THEN'
     (etac FalseE ORELSE'
-    hyp_subst_tac THEN'
+    hyp_subst_tac ctxt THEN'
     dresolve_tac Fwit_thms THEN'
     (etac FalseE ORELSE' atac))) 1);