--- a/src/Pure/ROOT.ML Mon Aug 26 21:53:56 2013 +0200
+++ b/src/Pure/ROOT.ML Mon Aug 26 21:56:08 2013 +0200
@@ -59,6 +59,7 @@
use "General/sha1.ML";
if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
+use "General/sha1_samples.ML";
use "PIDE/xml.ML";
use "PIDE/yxml.ML";