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