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