Bug fixing. If the inductive types do not occur in t, t is

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index bf97b47607f144dfc42e27f34b6bfc7468571f40..7270603a9636b7ebcd4be445ce9350b0757dfefb 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -1013,7 +1013,7 @@ class gui () =
             Helm_registry.get_opt_default Helm_registry.string ~default:"./"
               "matita.tptppath"
           in
-          let data = Matitaprover.p_to_ma ~filename:file ~tptppath in
+          let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in
           let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in
           script#assignFileName filename;
           source_view#source_buffer#begin_not_undoable_action ();