src/Tools/induct.ML

           | rename_params ((y, _) :: ys) = y :: rename_params ys;
         fun rename_asm A =
           let
             val xs = rename_params (Logic.strip_params A);
             val xs' =
-              (case List.filter (equal x) xs of
+              (case filter (fn x' => x' = x) xs of
                 [] => xs | [_] => xs | _ => index 1 xs);
           in Logic.list_rename_params (xs', A) end;
         fun rename_prop p =
           let val (As, C) = Logic.strip_horn p
           in Logic.list_implies (map rename_asm As, C) end;