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);