aux (aux [] ty) proofterm
in
let lit =
- match ty with
- | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
+ match B.is_eq ty with
+ | Some(ty,l,r) ->
let o = Order.compare_terms l r in
Terms.Equation (l, r, ty, o)
- | t -> Terms.Predicate t
+ | None -> Terms.Predicate ty
in
let proof = Terms.Exact proofterm in
fresh_unit_clause maxvar (0, lit, varlist, proof)