changeset 67202 | 30e863ad5a1a |
parent 64334 | 4fb8560df827 |
child 68087 | dac267cd51fe |
--- 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;