diff -r d0ad264f8c4f -r 9b0324e1293b Nominal/nominal_induct.ML
--- a/Nominal/nominal_induct.ML	Thu Nov 03 13:19:23 2011 +0000
+++ b/Nominal/nominal_induct.ML	Mon Nov 07 13:58:18 2011 +0000
@@ -75,7 +75,7 @@
         val ys =
           if p < n then []
           else map (tune o #1) (take (p - n) ps) @ xs;
-      in Logic.list_rename_params (ys, prem) end;
+      in Logic.list_rename_params ys prem end;
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn prop
       in Logic.list_implies (map rename As, C) end;