X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2Finterpretations.ml;h=28957074f058fa1fcdc1e99f976ab77cc0d66586;hb=70aa6dc959dc1d49f751c183367c3b73393c938b;hp=aaa87d0838fa946746e8a5db2b7c7cebfbda2866;hpb=cee0c3ca597ebbff2250674c255ed1bc909521fb;p=helm.git

diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml
index aaa87d083..28957074f 100644
--- a/matita/components/content/interpretations.ml
+++ b/matita/components/content/interpretations.ml
@@ -122,7 +122,7 @@ let add_interpretation (status : #status) dsc (symbol, args) appl_pattern =
   let status,id = fresh_id status in
   let ids =
    try
-    StringMap.find symbol status#interp_db.interpretations
+    id::StringMap.find symbol status#interp_db.interpretations
    with Not_found -> [id] in
   let status =
    status#set_interp_db { status#interp_db with