src/HOL/Tools/BNF/bnf_def.ML

           in
             Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
               unfold_thms_tac ctxt [#pred_set axioms] THEN
               HEADGOAL (EVERY' [REPEAT_DETERM o etac ctxt conjE,
                 etac ctxt (Lazy.force map_cong) THEN_ALL_NEW
-                  (etac ctxt bspec THEN' assume_tac ctxt)]))
+                  (etac ctxt @{thm bspec} THEN' assume_tac ctxt)]))
             |> Thm.close_derivation
           end;
 
         val map_cong_pred = Lazy.lazy mk_map_cong_pred;