diff -r 390e10ddadf2 -r f63c283cefaf src/HOLCF/ROOT.ML --- a/src/HOLCF/ROOT.ML Tue Nov 04 14:37:51 1997 +0100 +++ b/src/HOLCF/ROOT.ML Tue Nov 04 14:40:29 1997 +0100 @@ -14,14 +14,10 @@ use_thy "HOLCF"; -(* sections axioms, ops *) -use "ax_ops/holcflogic.ML"; -use "ax_ops/thy_axioms.ML"; -use "ax_ops/thy_ops.ML"; -use "ax_ops/thy_syntax.ML"; +use "HOLCFLogic"; +use "contconsts"; -(* sections domain, generated *) - +(* domain package *) use "domain/library.ML"; use "domain/syntax.ML"; use "domain/axioms.ML";