# HG changeset patch
# User wenzelm
# Date 918059815 -3600
# Node ID 9dac1ee185e37cc09dd2e1cb19be2aa99a3bce5b
# Parent  05d99c0bbfa0aa3f49349e611522e283928d7ccc
tidied load path handling;

diff -r 05d99c0bbfa0 -r 9dac1ee185e3 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";
diff -r 05d99c0bbfa0 -r 9dac1ee185e3 src/HOLCF/IOA/ABP/ROOT.ML
--- a/src/HOLCF/IOA/ABP/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IOA/ABP/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
@@ -9,6 +9,4 @@
 
 goals_limit := 1;
 
-loadpath:=["."];
-
 use_thy "Correctness";
diff -r 05d99c0bbfa0 -r 9dac1ee185e3 src/HOLCF/IOA/NTP/ROOT.ML
--- a/src/HOLCF/IOA/NTP/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IOA/NTP/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
@@ -9,6 +9,4 @@
 
 goals_limit := 1;
 
-loadpath:=["."];
-
 use_thy "Correctness";
diff -r 05d99c0bbfa0 -r 9dac1ee185e3 src/HOLCF/IOA/ROOT.ML
--- a/src/HOLCF/IOA/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IOA/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
@@ -3,18 +3,16 @@
     Author:     Olaf Mueller
     Copyright   1997  TU Muenchen
 
-This is the ROOT file for the formalization of a semantic model of I/O-Automata.
-
-See the README.html file for details.
-
-Should be executed in the subdirectory HOLCF/IOA/meta_theory.
+This is the ROOT file for the formalization of a semantic model of
+I/O-Automata.  See the README.html file for details.
 *)
 
+goals_limit := 1;
 
-goals_limit:=1;
+add_path "meta_theory";
 
-loadpath := ["meta_theory"];
+use_thy "Abstraction";
+use_thy "TrivEx";
+use_thy "TrivEx2";
 
-use_thy"Abstraction";
-use_thy"TrivEx";
-use_thy"TrivEx2";
\ No newline at end of file
+reset_path ();
diff -r 05d99c0bbfa0 -r 9dac1ee185e3 src/HOLCF/IOA/Storage/ROOT.ML
--- a/src/HOLCF/IOA/Storage/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
+++ b/src/HOLCF/IOA/Storage/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
@@ -8,6 +8,4 @@
 
 goals_limit := 1;
 
-loadpath:=["."];
-
 use_thy "Correctness";