diff --git a/src/transform/discriminate.ml b/src/transform/discriminate.ml index 5c93d5bf1bf1cea44f65bee50f313e3a465a737b..dc2ba1da0c0b67832c8a8a6bb7e85b7178197b12 100644 --- a/src/transform/discriminate.ml +++ b/src/transform/discriminate.ml @@ -57,7 +57,7 @@ module Lsmap = struct let add ls tyl tyv lsmap = if ls_equal ls ps_equ then lsmap else - if not (List.for_all Ty.ty_closed tyl) then lsmap else + if not (List.for_all Ty.ty_closed (oty_cons tyl tyv)) then lsmap else let newls = function | None -> Some (create_lsymbol (id_clone ls.ls_name) tyl tyv) | nls -> nls