- Print/Set commands removed

[helm.git] / matita / components / content / interpretations.ml

diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml
index aaa87d0838fa946746e8a5db2b7c7cebfbda2866..28957074f058fa1fcdc1e99f976ab77cc0d66586 100644 (file)
--- 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