HOL-ODE-Numerics.Refine_Dflt_No_Comp