Syntax of paramodulation parameters changed.

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 4dcf38b6d56fc6f032fb00bc9aa62481906c6a44..c7e5579f8038a80a5929f261ed8d45a657c09ebd 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -130,7 +130,7 @@ let rewritingstep ~dbd lhs rhs just conclude =
    match just with
       None ->
        Tactics.auto ~dbd
-        ~params:["paramodulation","on"; "timeout","3"]
+        ~params:["paramodulation","1"; "timeout","3"]
     | Some just -> Tactics.apply just
   in
    match lhs with