src/Pure/General/sha1.ML
changeset 62663 bea354f6ff21
parent 57638 ed58e740a699
child 62666 00aff1da05ae
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
   137 val digest = Digest o digest_string;
   137 val digest = Digest o digest_string;
   138 fun rep (Digest s) = s;
   138 fun rep (Digest s) = s;
   139 
   139 
   140 val fake = Digest;
   140 val fake = Digest;
   141 
   141 
       
   142 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
       
   143 
   142 end;
   144 end;