Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 =
isabelle