| changeset 33955 | fff6f11b1f09 |
| parent 33368 | b1cf34f1855c |
| child 33957 | e9afca2118d4 |
--- a/src/Tools/induct_tacs.ML Tue Nov 24 14:37:23 2009 +0100 +++ b/src/Tools/induct_tacs.ML Tue Nov 24 17:28:25 2009 +0100 @@ -59,7 +59,7 @@ fun prep_inst (concl, xs) = let val vs = Induct.vars_of concl - in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end; + in map_filter prep_var ((uncurry drop) (length vs - length xs, vs) ~~ xs) end; in