X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=7b1e2c50869f4e5b93fbc112f3b116515d58825a;hb=d4a074601a61f35ab146a1b97014768683e7ee65;hp=9cfbbc8c0a184b75a47a68d7a2d3ab12b6b49c34;hpb=fd4f563ed52c644b14b1e6a4045fca1c241444a7;p=helm.git

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index 9cfbbc8c0..7b1e2c508 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -57,9 +57,9 @@ class virtual status =
 let eval_with_new_aliases status f =
  let status =
   status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
- let res = f status in
- let new_aliases = status#disambiguate_db.new_aliases in
-  new_aliases,res
+ let new_status = f status in
+ let new_aliases = new_status#disambiguate_db.new_aliases in
+  new_aliases,new_status
 ;;
 
 let dump_aliases out msg status =