--- a/src/HOL/ROOT.ML Thu Mar 11 12:34:10 1999 +0100 +++ b/src/HOL/ROOT.ML Thu Mar 11 13:20:35 1999 +0100 @@ -76,5 +76,3 @@ print_depth 8; Goal "True"; (*leave subgoal package empty*) - -val HOL_build_completed = (); (*indicate successful build*)