fixed defaultauto behaviour. not the cache is preserveed

diff --git a/components/tactics/paramodulation/equality_retrieval.ml b/components/tactics/paramodulation/equality_retrieval.ml
index e0e92b408db2ad206b032ea7809ca83a90ef17ad..962304d41ac8d7c28df9dc9cfffebdd6242aac18 100644 (file)
--- a/components/tactics/paramodulation/equality_retrieval.ml
+++ b/components/tactics/paramodulation/equality_retrieval.ml
@@ -136,7 +136,7 @@ let equations_blacklist = UriManager.UriSet.empty;;
 (*****************************************************************)
 exception AutoFailure of AutoCache.cache * int
 
-let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;; 
+let default_auto maxm _ _ _ c _ = [],c,maxm ;; 
 
 let close_hypothesis_of_term context metasenv oldnewmeta term cache auto fast = 
   let head, metasenv, args, newmeta =