src/HOLCF/ROOT.ML
changeset 6349 f7750d816c21
parent 5517 863f56450888
child 12036 49f6c49454c2
--- a/src/HOLCF/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOLCF/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
@@ -7,8 +7,6 @@
 Should be executed in subdirectory HOLCF.
 *)
 
-HOL_build_completed;    (* Cause HOLCF to fail if HOL did *)
-
 val banner = "HOLCF";
 writeln banner;
 
@@ -28,5 +26,3 @@
 use "domain/interface.ML";
 
 print_depth 10;  
-
-val HOLCF_build_completed = (); (*indicate successful build*)