--- a/src/HOLCF/IMP/ROOT.ML Tue May 30 16:03:09 2000 +0200
+++ b/src/HOLCF/IMP/ROOT.ML Tue May 30 16:08:38 2000 +0200
@@ -4,5 +4,4 @@
Copyright 1997 TU Muenchen
*)
-use_thy "../../HOL/IMP/Natural";
-use_thy "HoareEx";
+with_path "../../HOL/IMP" time_use_thy "HoareEx";