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