X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=3601f4c443a5b94f3685bd7414c88f9f89c3d9aa;hb=132d053caaeb9f8311fb0c807a9d7fd8d7acc827;hp=dbdd2131304c1ec34b4da5a0e717fa24e7743ab9;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index dbdd21313..3601f4c44 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -250,7 +250,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
      match obj with
      | NotationPt.Inductive (_,(name,_,_,_)::_)
      | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
-     | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+     | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
      | NotationPt.Inductive _ -> assert false
    in
      NUri.uri_of_string (baseuri ^ "/" ^ name)