src/HOL/Codatatype/Tools/bnf_wrap.ML

               in
                 Local_Defs.fold lthy [sel_def]
                   (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm)
               end;
             fun mk_thms k xs goal_case case_thm sel_defs =
-              map2 (mk_thm k xs goal_case case_thm) xs sel_defs;
+              map2 (mk_thm k xs (strip_all_body goal_case) case_thm) xs sel_defs;
           in
             map5 mk_thms ks xss goal_cases case_thms sel_defss
           end;
 
         fun mk_unique_disc_def k =