src/Pure/ROOT.ML
changeset 53212 387b9f7cb0ac
parent 53192 04df1d236e1c
child 53707 d1c6bff9ff58
     1.1 --- a/src/Pure/ROOT.ML	Mon Aug 26 21:53:56 2013 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Aug 26 21:56:08 2013 +0200
     1.3 @@ -59,6 +59,7 @@
     1.4  
     1.5  use "General/sha1.ML";
     1.6  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
     1.7 +use "General/sha1_samples.ML";
     1.8  
     1.9  use "PIDE/xml.ML";
    1.10  use "PIDE/yxml.ML";