--- a/src/HOL/MiniML/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/MiniML/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -6,8 +6,6 @@
Type inference for MiniML
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
-
writeln"Root file for HOL/MiniML";
time_use_thy "W";