X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgHelena.ml;h=43146aebb236db2af9379e88aec230c2fa3d5f72;hb=2e97c767bc072f5ba238725ff1f738fc91a0135a;hp=07aa996013e7ff96655a5e0a32991cfb82574c92;hpb=88977b2d546e547e23b046792fe2ad8f6ff192a4;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgHelena.ml b/helm/software/helena/src/basic_rg/brgHelena.ml
index 07aa99601..43146aebb 100644
--- a/helm/software/helena/src/basic_rg/brgHelena.ml
+++ b/helm/software/helena/src/basic_rg/brgHelena.ml
@@ -304,7 +304,6 @@ let close_out_tj3 och () =
       end
    in
    let chunks = out_list och 1 true size (List.rev !uris) in
-   out_clause och "main :- grundlagen.";
    KP.fprintf och "grundlagen :-\n";
    out_chunks och (pred chunks) 1;
    close_out och
@@ -325,10 +324,9 @@ let open_out_lp1 fname =
 let open_out_lp2 fname =
    let dir = KF.concat !G.manager_dir base in 
    let path = KF.concat dir fname in
-   let och = open_out (path ^ "2" ^ ext_lp) in
+   let och = open_out (path ^ "b_ld3" ^ ext_lp) in
    out_preamble och;
    out_top_comment och version;
-   out_clause och "accumulate helena.";
    output_entity_lp2 och, close_out_lp2 och
 
 let open_out_tj2 fname =