src/FOL/FOL.ML

--- a/src/FOL/FOL.ML	Fri Jan 03 10:48:28 1997 +0100
+++ b/src/FOL/FOL.ML	Fri Jan 03 15:01:55 1997 +0100
@@ -67,3 +67,9 @@
   [ (rtac conjE 1),
     (REPEAT (DEPTH_SOLVE_1 
         (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
+
+
+(*Thus, assignments to the references claset and simpset are recorded
+  with theory "FOL".  These files cannot be loaded directly in ROOT.ML.*)
+use "cladata.ML";
+use "simpdata.ML";