diff -r 6f549f5e7066 -r e9afca2118d4 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Tools/induct.ML	Wed Nov 25 09:13:46 2009 +0100
@@ -280,11 +280,11 @@
 
 fun align_left msg xs ys =
   let val m = length xs and n = length ys
-  in if m < n then error msg else ((uncurry take) (n, xs) ~~ ys) end;
+  in if m < n then error msg else (take n xs ~~ ys) end;
 
 fun align_right msg xs ys =
   let val m = length xs and n = length ys
-  in if m < n then error msg else ((uncurry drop) (m - n, xs) ~~ ys) end;
+  in if m < n then error msg else (drop (m - n) xs ~~ ys) end;
 
 
 (* prep_inst *)