| changeset 35628 | f1456d045151 |
| parent 35626 | 06197484c6ad |
| child 35669 | a91c7ed801b8 |
--- a/src/Pure/ROOT.ML Sun Mar 07 15:49:49 2010 +0100 +++ b/src/Pure/ROOT.ML Sun Mar 07 15:51:29 2010 +0100 @@ -52,6 +52,11 @@ use "General/xml.ML"; use "General/yxml.ML"; +use "General/sha1.ML"; +if String.isPrefix "polyml" ml_system +then use "General/sha1_polyml.ML" +else (); + (* concurrency within the ML runtime *)