src/Tools/induct.ML
changeset 28375 c879d88d038a
parent 28083 103d9282a946
child 28965 1de908189869
--- a/src/Tools/induct.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Tools/induct.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -478,7 +478,7 @@
           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 =