src/Tools/induct.ML
changeset 45328 e5b33eecbf6e
parent 45156 a9b6c2ea7bec
child 45375 7fe19930dfc9
     1.1 --- a/src/Tools/induct.ML	Thu Nov 03 22:23:41 2011 +0100
     1.2 +++ b/src/Tools/induct.ML	Thu Nov 03 22:51:37 2011 +0100
     1.3 @@ -627,7 +627,7 @@
     1.4              val xs' =
     1.5                (case filter (fn x' => x' = x) xs of
     1.6                  [] => xs | [_] => xs | _ => index 1 xs);
     1.7 -          in Logic.list_rename_params (xs', A) end;
     1.8 +          in Logic.list_rename_params xs' A end;
     1.9          fun rename_prop p =
    1.10            let val (As, C) = Logic.strip_horn p
    1.11            in Logic.list_implies (map rename_asm As, C) end;