Fixed bug in eta_subterm

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 71f493545df93edce3e4a9b844b838b3b54e2c66..82c4b3803e4a0868e6e96eb58d935b9cae146628 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -343,9 +343,9 @@ let rec eta_subterm sub t =
      eta_subterm sub (u :> nf)
      || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
      || List.exists (eta_subterm sub) (args :> nf list)
-  | `I(v, args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
-   | `Var v' -> v = v'
-   | `I(v', args') -> v = v'
+  | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
+   | `Var(v',_) -> v = v'
+   | `I((v',_), args') -> v = v'
     && Listx.length args' < Listx.length args
     && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args :> nf list)) (Listx.to_list args' :> nf list))
    | _ -> false