X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=42cf063b64f08b3e352693d7a30bebff78025e95;hb=abdfd617eb0beb6961eea78e8f3b8cad73d43fde;hp=c5bb640a2ba8bdb5c532f7bcf89a3686c0c29fa9;hpb=320c0f89a7e31e996b6eff2b4165eb74e8141cec;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index c5bb640a2..42cf063b6 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -272,7 +272,12 @@ module Superposition (B : Orderings.Blob) =
     let rec demodulate bag (id, literal, vl, pr) table =
       debug (lazy ("demodulate " ^ (string_of_int id)));
        match literal with
-      | Terms.Predicate t -> assert false
+      | Terms.Predicate t -> (* assert false *)
+	  let bag,_,id1 =
+	    visit bag [] (fun x -> x) id t (ctx_demod table vl)
+	  in          
+	  let cl,_,_ = Terms.get_from_bag id1 bag in
+	    bag,cl
       | Terms.Equation (l,r,ty,_) ->
           let bag,l,id1 = 
 	    visit bag [2]