# HG changeset patch
# User wenzelm
# Date 1513258496 -3600
# Node ID 30e863ad5a1a3ea781ca2f1629cae5576ab4d284
# Parent  4cffa4791ef7a30b43edc3eb0d181b622a541239
proper exception;

diff -r 4cffa4791ef7 -r 30e863ad5a1a src/Pure/General/sha1.ML
--- 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;