# HG changeset patch
# User paulson
# Date 962182813 -7200
# Node ID 8f975d9c1046ac16720a426960398a8f0647ddea
# Parent  6f8499d86d4fdf98b44f584b25dbf054ae0ddd6e
simplified slightly by using dependencies better in theories

diff -r 6f8499d86d4f -r 8f975d9c1046 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Wed Jun 28 10:58:06 2000 +0200
+++ b/src/ZF/ROOT.ML	Wed Jun 28 11:00:13 2000 +0200
@@ -26,22 +26,14 @@
 use     "Tools/cartprod";
 use_thy "Fixedpt";
 use     "Tools/inductive_package";
-use_thy "Inductive";
 use     "Tools/induct_tacs";
 use     "Tools/primrec_package";
+use_thy "Inductive";
 use_thy "QUniv";
 use     "Tools/datatype_package";
-use_thy "Datatype";
-use_thy "InfDatatype";
-use_thy "List";
-
-(*Integers & binary integer arithmetic*)
-cd "Integ";
-use_thy "Bin";
-cd "..";
 
 (*the all-in-one theory*)
-use_thy "Main";
+with_path "Integ" use_thy "Main";
 
 simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);