tuned;

--- a/src/HOL/ROOT.ML	Fri Sep 25 12:03:11 1998 +0200
+++ b/src/HOL/ROOT.ML	Fri Sep 25 12:12:07 1998 +0200
@@ -52,7 +52,7 @@
 use "Tools/datatype_abs_proofs.ML";
 use "Tools/datatype_package.ML";
 use "Tools/primrec_package.ML";
-use_thy"Datatype";
+use_thy "Datatype";
 
 use_thy "Arith";
 use "arith_data.ML";
@@ -65,7 +65,7 @@
 
 cd "Integ";
 use_thy "IntDef";
-use     "simproc";
+use "simproc.ML";
 use_thy "Bin";
 cd "..";