src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

             val t = #user_eqn sel_eqn
               |> abstract 0 (List.rev (#fun_args sel_eqn)) (* FIXME do this in dissect_\<dots> *)
               |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
               |> curry Logic.list_all (map dest_Free (#fun_args sel_eqn));
           in
-            mk_primcorec_eq_tac lthy def_thms sel_corec k m exclsss
+            mk_primcorec_ctr_or_sel_tac lthy def_thms sel_corec k m exclsss
               nested_maps nested_map_idents nested_map_comps
             |> K |> Goal.prove lthy [] [] t
           end;
 
         val disc_notes =