author | wenzelm |
Thu, 14 Dec 2017 14:34:56 +0100 | |
changeset 67202 | 30e863ad5a1a |
parent 67201 | 4cffa4791ef7 |
child 67203 | 85784e16bec8 |
--- a/src/Pure/General/sha1.ML Thu Dec 14 14:28:27 2017 +0100 +++ b/src/Pure/General/sha1.ML Thu Dec 14 14:34:56 2017 +0100 @@ -190,7 +190,7 @@ val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep); fun digest_string str = digest_string_external str - handle CInterface.Foreign msg => + handle Foreign.Foreign msg => (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); digest_string_internal str); val digest = Digest o digest_string;