src/HOL/IMP/ROOT.ML

--- a/src/HOL/IMP/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/IMP/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
@@ -4,9 +4,8 @@
     Copyright   1995 TUM
 *)
 
-HOL_build_completed;    (*Make examples fail if HOL did*)
+writeln"Root file for HOL/IMP";
 
-writeln"Root file for HOL/IMP";
 set proof_timing;
 time_use_thy "Expr";
 time_use_thy "Transition";