diff -r a78ce0c6e191 -r 00aff1da05ae src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Mar 18 16:38:40 2016 +0100
+++ b/src/Pure/ROOT.ML	Fri Mar 18 17:11:30 2016 +0100
@@ -143,10 +143,7 @@
 use "General/socket_io.ML";
 use "General/seq.ML";
 use "General/timing.ML";
-
 use "General/sha1.ML";
-use "General/sha1_polyml.ML";
-use "General/sha1_samples.ML";
 
 val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;