From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 31 May 2007 15:02:52 +0000 (+0000)
Subject: Bug fixed: wrong id.
X-Git-Tag: make_still_working~6266
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7dbc6d6fe71f6967f5ad31528a629dc89e6d8160;p=helm.git

Bug fixed: wrong id.
---

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index a2e7622ea..1b8c287fa 100644
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -494,7 +494,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             { proof' with
                K.proof_name = None;
                K.proof_context = 
-                 ((build_def_item seed id n s ids_to_inner_sorts 
+                 ((build_def_item seed (get_id s) n s ids_to_inner_sorts 
                    ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
                  ::proof'.K.proof_context;
             }