src/Tools/induct_tacs.ML
changeset 33957 e9afca2118d4
parent 33955 fff6f11b1f09
child 35625 9c818cab0dd0
--- a/src/Tools/induct_tacs.ML	Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Tools/induct_tacs.ML	Wed Nov 25 09:13:46 2009 +0100
@@ -59,7 +59,7 @@
 
 fun prep_inst (concl, xs) =
   let val vs = Induct.vars_of concl
-  in map_filter prep_var ((uncurry drop) (length vs - length xs, vs) ~~ xs) end;
+  in map_filter prep_var (drop (length vs - length xs) vs ~~ xs) end;
 
 in