src/Pure/Proof/extraction.ML
changeset 33955 fff6f11b1f09
parent 33832 cff42395c246
child 33957 e9afca2118d4
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Nov 24 17:28:25 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 (Library.take (n, vars) ~~ Library.take (n, ts)) ([], []) end;
     1.8 +      in fold_rev add_args ((uncurry take) (n, vars) ~~ (uncurry 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);