X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=3601f4c443a5b94f3685bd7414c88f9f89c3d9aa;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=dbdd2131304c1ec34b4da5a0e717fa24e7743ab9;hpb=225887a9f23aac79d4cca907da026917b7df04dc;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)