--- a/src/HOL/MiniML/ROOT.ML Tue May 30 16:03:09 2000 +0200 +++ b/src/HOL/MiniML/ROOT.ML Tue May 30 16:08:38 2000 +0200 @@ -6,6 +6,4 @@ Type inference for MiniML *) -writeln"Root file for HOL/MiniML"; - time_use_thy "W";