# HG changeset patch
# User wenzelm
# Date 869829525 -7200
# Node ID b2b9a9ddb9ccd3d3b39e88074823640396afd805
# Parent  9715b6e3ec5f24266333b4d5a5cbab96d36a663e
load simplifier.ML (again);

diff -r 9715b6e3ec5f -r b2b9a9ddb9cc src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Fri Jul 25 13:18:09 1997 +0200
+++ b/src/FOL/ROOT.ML	Fri Jul 25 13:18:45 1997 +0200
@@ -13,6 +13,7 @@
 
 print_depth 1;  
 
+use "../Provers/simplifier.ML";
 use "../Provers/splitter.ML";
 use "../Provers/ind.ML";
 use "../Provers/hypsubst.ML";
diff -r 9715b6e3ec5f -r b2b9a9ddb9cc src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Jul 25 13:18:09 1997 +0200
+++ b/src/HOL/ROOT.ML	Fri Jul 25 13:18:45 1997 +0200
@@ -16,6 +16,7 @@
 use "../Pure/section_utils.ML";
 use "thy_syntax.ML";
 
+use "../Provers/simplifier.ML";
 use "../Provers/splitter.ML";
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";