src/HOL/ROOT.ML

 use "Tools/datatype_prop.ML";
 use "Tools/datatype_rep_proofs.ML";
 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";
 
 use_thy "Recdef";

 use "sys.sml";
 cd "$ISABELLE_HOME/src/HOL";
 
 cd "Integ";
 use_thy "IntDef";
-use     "simproc";
+use "simproc.ML";
 use_thy "Bin";
 cd "..";
 
 (*the all-in-one theory*)
 use_thy "Main";