added filtering criteria on differences between number of constants in

[helm.git] / helm / ocaml / metadata / metadataDb.ml

diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index 4b7664c224fdac212b9e5700b0fa800c74de4c73..30e5912d822720a1cdbb24d876b6f47c1c249b4a 100644 (file)
--- a/helm/ocaml/metadata/metadataDb.ml
+++ b/helm/ocaml/metadata/metadataDb.ml
@@ -76,7 +76,7 @@ let insert_const_no dbd uri =
         SELECT \"%s\",COUNT(DISTINCT h_occurrence)
         FROM %s
         WHERE NOT (h_position=\"%s\") AND (source = \"%s\")"
-      (conclno_hyp_tbl ()) uri (obj_tbl ()) inbody_pos uri
+      (fullno_tbl ()) uri (obj_tbl ()) inbody_pos uri
   in
   ignore (Mysql.exec dbd inconcl_no);
   ignore (Mysql.exec dbd concl_hyp)
@@ -121,7 +121,7 @@ let index_inductive_def ~dbd =
     end
 
 let tables_to_clean =
-  [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl]
+  [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; fullno_tbl; name_tbl]
 
 let clean ~(dbd:Mysql.dbd) =
   let owned_uris =  (* list of uris in list-of-columns format *)