src/FOLP/ROOT.ML
changeset 1008 fa11e1e28bd3
parent 393 02b27671b899
child 1296 ae31bb7774a7
--- 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 ***)