X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=95d6082d0b4296bd1ee12d7649cb8b0c11122ab4;hb=dd4bd89108bea062338a0f04ea616432edaad13c;hp=4476d562a949d0e9a82e0bc69f49dfb8dacc3649;hpb=46ee64f692a1e5e65864ebb82ec875e8d115843c;p=helm.git

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index 4476d562a..95d6082d0 100644
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -334,7 +334,7 @@ let domain_of_term ~context term =
 let domain_of_obj ~context ast =
  assert (context = []);
   match ast with
-   | Ast.Theorem (_,_,ty,bo,_) ->
+   | Ast.Theorem (_,ty,bo,_) ->
       domain_of_term [] ty
       @ (match bo with
           None -> []