src/HOL/Tools/Function/function_elims.ML

         fun unstrip rl =
           rl
           |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) arg_vars
           |> Thm.forall_intr P
       in
-        map unstrip (elim_stripped :: bool_elims)
+        map (unstrip #> Thm.solve_constraints) (elim_stripped :: bool_elims)
       end;
   in
     map_index mk_partial_elim_rule fs
   end;