# HG changeset patch
# User lcp
# Date 797159555 -7200
# Node ID fa11e1e28bd341c5d05ddff959a40eb3bb60358f
# Parent  79d316b160fa98c8067439d0bfb9ccd0ee893ef8
Loads the local hypsubst.ML.  No longer loads ../Provers/ind.ML,
which was never used.

diff -r 79d316b160fa -r fa11e1e28bd3 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Thu Apr 06 11:09:15 1995 +0200
+++ b/src/FOLP/ROOT.ML	Thu Apr 06 11:12:35 1995 +0200
@@ -18,10 +18,9 @@
 use_thy "IFOLP";
 use_thy "FOLP";
 
-use "../Provers/hypsubst.ML";
+use "hypsubst.ML";
 use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
 use "simp.ML";	         (* Patched 'cos matching won't instantiate proof *)
-use "../Provers/ind.ML";
 
 
 (*** Applying HypsubstFun to generate hyp_subst_tac ***)