src/HOL/Integ/ROOT.ML

--- a/src/HOL/Integ/ROOT.ML	Wed Jun 24 13:59:45 1998 +0200
+++ b/src/HOL/Integ/ROOT.ML	Thu Jun 25 13:57:34 1998 +0200
@@ -6,7 +6,4 @@
 The Integers in HOL (ported from ZF by Riccardo Mattolini)
 *)
 
-HOL_build_completed;    (*Cause examples to fail if HOL did*)
-
 time_use_thy "Bin";
-time_use_thy "IntRing";