diff -r fdcbeaddd5fc -r f7750d816c21 src/ZF/Resid/ROOT.ML
--- a/src/ZF/Resid/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
+++ b/src/ZF/Resid/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
@@ -12,11 +12,9 @@
 J. Functional Programming 4(3) 1994, 371-394.
 *)
 
-ZF_build_completed;     (*Make examples fail if ZF did*)
+writeln"Root file for ZF/Resid";
 
-writeln"Root file for ZF/Resid";
 set proof_timing;
-
 time_use_thy "Conversion";
 
 writeln"END: Root file for ZF/Resid";