src/HOLCF/IMP/ROOT.ML

--- a/src/HOLCF/IMP/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IMP/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
@@ -4,15 +4,8 @@
     Copyright   1997  TU Muenchen
 *)
 
-(*Load theories from ../meta_theory without generating HTML files
-  (has already been done by HOL/IMP/ROOT.ML)*)
-val old_make_html = !make_html;
-make_html := false;
-loadpath := ["../../HOL/IMP"];
-
+add_path "../../HOL/IMP";
 use_thy "Natural";
 
-make_html := old_make_html;
-loadpath := ["."];
-
+reset_path ();
 use_thy "HoareEx";