X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=c350f38c41ab03c6a735643e676d2e53809e1009;hb=6cc401c4136bafb6515bd39d86db6b5a917318bf;hp=508411d2847b1b84083141efa5bbe14aed16a8fa;hpb=e085135177f7b3b74b410d47a4f3bca1784b60b1;p=helm.git

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index 508411d28..c350f38c4 100644
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -442,19 +442,22 @@ let set_active_interpretations ids =
 
 exception Interpretation_not_found
 
-let lookup_interpretations symbol =
+let lookup_interpretations ?(sorted=true) symbol =
   try
-   HExtlib.list_uniq
-    (List.sort Pervasives.compare
-     (List.map
-      (fun id ->
-        let (dsc, _, args, appl_pattern) =
-          try
-            Hashtbl.find !level2_patterns32 id
-          with Not_found -> assert false 
-        in
-        dsc, args, appl_pattern)
-      !(Hashtbl.find !interpretations symbol)))
+    let raw = 
+      List.map (
+        fun id ->
+          let (dsc, _, args, appl_pattern) =
+            try
+              Hashtbl.find !level2_patterns32 id
+            with Not_found -> assert false 
+          in
+          dsc, args, appl_pattern
+      )
+      !(Hashtbl.find !interpretations symbol)
+    in
+    if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+              else raw
   with Not_found -> raise Interpretation_not_found
 
 let remove_interpretation id =