From 7dbc6d6fe71f6967f5ad31528a629dc89e6d8160 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 May 2007 15:02:52 +0000 Subject: [PATCH] Bug fixed: wrong id. --- helm/software/components/acic_content/acic2content.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; } -- 2.39.2