# HG changeset patch
# User wenzelm
# Date 878556525 -3600
# Node ID 8cdf672a83e8fdc55b796dbb613d3d893ff8f755
# Parent  6fd0f439e50e347f8c166b7b017473c469656f11
moved cladata.ML, simpdata.ML to ROOT.ML;

diff -r 6fd0f439e50e -r 8cdf672a83e8 src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Mon Nov 03 12:28:14 1997 +0100
+++ b/src/FOL/FOL.ML	Mon Nov 03 12:28:45 1997 +0100
@@ -70,8 +70,3 @@
     (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";
diff -r 6fd0f439e50e -r 8cdf672a83e8 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Mon Nov 03 12:28:14 1997 +0100
+++ b/src/FOL/ROOT.ML	Mon Nov 03 12:28:45 1997 +0100
@@ -43,6 +43,9 @@
 
 use_thy "FOL";
 
+use "cladata.ML";
+use "simpdata.ML";
+
 qed_goal "ex1_functional" FOL.thy
     "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
  (fn _ => [ (deepen_tac FOL_cs 0 1) ]);