src/Pure/Proof/extraction.ML
changeset 33957 e9afca2118d4
parent 33955 fff6f11b1f09
child 35424 08c37d7bd2ad
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Nov 24 17:28:44 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Nov 25 09:13:46 2009 +0100
     1.3 @@ -461,7 +461,7 @@
     1.4              end
     1.5            else (vs', tye)
     1.6  
     1.7 -      in fold_rev add_args ((uncurry take) (n, vars) ~~ (uncurry take) (n, ts)) ([], []) end;
     1.8 +      in fold_rev add_args (take n vars ~~ take n ts) ([], []) end;
     1.9  
    1.10      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
    1.11      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);