X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;h=244cd1d728975ebc22f000402bf99e5e589329ea;hb=05b509909ee5b61dbfca46d1239d64556af5ba2e;hp=a19fa67c20d3281967d8ec77a754f84ede510a51;hpb=a7237500e8a2a4237a6ae8ba4b8301f7bbcb6acb;p=helm.git

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index a19fa67c2..244cd1d72 100644
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -237,8 +237,9 @@ let ng_generate_tactics fv ueq_case context arities =
       (fun _ -> 
         [GA.Executable(floc,GA.NTactic(floc, 
           [GA.NApply (floc,
-            PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
-              PT.Implicit;PT.Implicit]);GA.NBranch floc]));
+            PT.Appl
+             [mk_ident "ex_intro";PT.Implicit `JustOne;PT.Implicit `JustOne;
+              PT.Implicit `JustOne;PT.Implicit `JustOne]);GA.NBranch floc]));
          GA.Executable(floc,GA.NTactic(floc, 
           [GA.NPos (floc,[2])]))])
       fv))