# HG changeset patch
# User paulson
# Date 859987101 -7200
# Node ID 0a648ebbf6d4dca4d5022d5ec03bb33b2662174e
# Parent  77daca16b2f462c53e28052f915bec814bdb41bc
Now loads blast.ML

diff -r 77daca16b2f4 -r 0a648ebbf6d4 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Wed Apr 02 15:14:37 1997 +0200
+++ b/src/FOL/ROOT.ML	Wed Apr 02 15:18:21 1997 +0200
@@ -19,9 +19,11 @@
 use "../Provers/ind.ML";
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";
+use "../Provers/blast.ML";
 
 use_thy "IFOL";
 
+(** Applying HypsubstFun to generate hyp_subst_tac **)
 structure Hypsubst_Data =
   struct
   structure Simplifier = Simplifier