diff -r 2209eb5bb56b -r b67c8e01ae04 IMP/ROOT.ML
--- a/IMP/ROOT.ML	Thu Apr 06 11:24:11 1995 +0200
+++ b/IMP/ROOT.ML	Thu Apr 06 11:27:54 1995 +0200
@@ -17,6 +17,5 @@
 writeln"Root file for HOL/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
-(time_use_thy "Properties";
- time_use_thy "Equiv"
-)  handle _ => exit 1;
+time_use_thy "Properties";
+time_use_thy "Equiv";