proper exception;
authorwenzelm
Thu Dec 14 14:34:56 2017 +0100 (17 months ago)
changeset 6720230e863ad5a1a
parent 67201 4cffa4791ef7
child 67203 85784e16bec8
proper exception;
src/Pure/General/sha1.ML
     1.1 --- a/src/Pure/General/sha1.ML	Thu Dec 14 14:28:27 2017 +0100
     1.2 +++ b/src/Pure/General/sha1.ML	Thu Dec 14 14:34:56 2017 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4  val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
     1.5  
     1.6  fun digest_string str = digest_string_external str
     1.7 -  handle CInterface.Foreign msg =>
     1.8 +  handle Foreign.Foreign msg =>
     1.9      (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); digest_string_internal str);
    1.10  
    1.11  val digest = Digest o digest_string;