X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_procedural%2FproceduralClassify.ml;h=4c0014d2e320e4e214aa511f66f1694ee9b6ac59;hb=24dd4569daf1d35bffaa813b8164058d8643f14d;hp=755176e5c50cc4d4d280fcee4b373089ebbcb485;hpb=1dd6fc8c5d7bde039972a208c5eb03d3ea8303dd;p=helm.git

diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml
index 755176e5c..4c0014d2e 100644
--- a/components/acic_procedural/proceduralClassify.ml
+++ b/components/acic_procedural/proceduralClassify.ml
@@ -78,12 +78,13 @@ let classify_conclusion vs =
  
 let classify c t =
 try   
-   let vs, h = PEH.split_with_whd (c, t) in
+   let vs, h = PEH.split_with_normalize (c, t) in
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in
+      let isf = argsno > 0 || H.is_sort v in
       let iu = H.is_unsafe h (List.hd vs) in
-      (I.get_rels_from_premise h v, I.S.empty, argsno > 0 && iu) :: b, succ h
+      (I.get_rels_from_premise h v, I.S.empty, isf && iu) :: b, succ h
    in
    let l, h = List.fold_left map ([], 0) vs in
    let b = Array.of_list (List.rev l) in