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 =