src/Tools/induct.ML

--- a/src/Tools/induct.ML	Thu Nov 03 22:23:41 2011 +0100
+++ b/src/Tools/induct.ML	Thu Nov 03 22:51:37 2011 +0100
@@ -627,7 +627,7 @@
             val xs' =
               (case filter (fn x' => x' = x) xs of
                 [] => xs | [_] => xs | _ => index 1 xs);
-          in Logic.list_rename_params (xs', A) end;
+          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;