I do not know why, but

[helm.git] / components / tptp_grafite / tptp2grafite.ml

diff --git a/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml
index 3ed457d958dd64d25ee7d29ab111ad53574563c2..a7f3a85238fcf527172074b8266caf6396e1291b 100644 (file)
--- a/components/tptp_grafite/tptp2grafite.ml
+++ b/components/tptp_grafite/tptp2grafite.ml
@@ -247,7 +247,7 @@ let convert_ast statements context = function
           statements @ [
             GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
             GA.Executable(floc,GA.Tactic(floc, Some
-             (GA.Intros (floc,None,[])),GA.Dot(floc)))] @
+             (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
           (if fv <> [] then     
             (List.flatten
               (List.map 
@@ -260,10 +260,10 @@ let convert_ast statements context = function
            else [])@
             [GA.Executable(floc,GA.Tactic(floc, Some (
               if ueq_case then
-                GA.Auto (floc,["paramodulation","";
+                GA.AutoBatch (floc,["paramodulation","";
                   "timeout",string_of_int !paramod_timeout])
               else
-                GA.Auto (floc,["depth",string_of_int !depth])
+                GA.AutoBatch (floc,["depth",string_of_int !depth])
             ),
               GA.Dot(floc)));
             GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,