metis.ml: qualify sqrt by Stdlib (one occurrence)

[fblanqui]

Hi. I don't know exactly why but I get some typing error when tracing HOL-Light proofs with https://github.com/Deducteam/hol2dk because the only occurrence of sqrt in metis.ml is not qualified and thus depends on the context it is evaluated, which I believe is not what is wanted. This PR proposes to fix this.

[fblanqui]

Remark: I see that hol_lib.ml is defining float_sqrt as (non qualified) sqrt too, and float_fabs as (unqualified) abs_float. These two functions are used only in Jordan/float.ml (twice). Perhaps, these two definitions could be removed and replaced by Stdlib.sqrt and Stdlib.abs_float respectively? I can update this PR accordingly if you want.

[jargh]

I agree we shouldn't have the simple unqualified name like this, so I'm all in favour of changing. But for the sake of compatibility with older OCamls I'd prefer to use the float_sqrt function that you noticed - having this local definition is maybe a bit hacky but it I think it's nice to be able to load the same source into even (for example) OCaml 4.05, where this picks up Pervasives.sqrt. See comments in https://github.com/jrh13/hol-light/blob/master/hol_lib.ml#L16-L26.