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*)