src/Pure/General/sha1.ML
changeset 67202 30e863ad5a1a
parent 64334 4fb8560df827
child 68087 dac267cd51fe
equal deleted inserted replaced
67201:4cffa4791ef7 67202:30e863ad5a1a
   188 val fake = Digest;
   188 val fake = Digest;
   189 
   189 
   190 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
   190 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
   191 
   191 
   192 fun digest_string str = digest_string_external str
   192 fun digest_string str = digest_string_external str
   193   handle CInterface.Foreign msg =>
   193   handle Foreign.Foreign msg =>
   194     (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); digest_string_internal str);
   194     (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); digest_string_internal str);
   195 
   195 
   196 val digest = Digest o digest_string;
   196 val digest = Digest o digest_string;
   197 
   197 
   198 
   198