summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 08 Oct 2014 14:34:30 +0200 | |

changeset 58633 | 8529745af3dc |

parent 58632 | 08536219d3a2 |

child 58634 | 9f10d82e8188 |

tuned;

--- a/src/Pure/library.ML Wed Oct 08 13:55:43 2014 +0200 +++ b/src/Pure/library.ML Wed Oct 08 14:34:30 2014 +0200 @@ -531,19 +531,19 @@ | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys | map2 _ _ _ = raise ListPair.UnequalLengths; -fun fold2 f [] [] z = z +fun fold2 _ [] [] z = z | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z) - | fold2 f _ _ _ = raise ListPair.UnequalLengths; + | fold2 _ _ _ _ = raise ListPair.UnequalLengths; -fun fold_rev2 f [] [] z = z +fun fold_rev2 _ [] [] z = z | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z) - | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths; + | fold_rev2 _ _ _ _ = raise ListPair.UnequalLengths; -fun forall2 P [] [] = true +fun forall2 _ [] [] = true | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys - | forall2 P _ _ = raise ListPair.UnequalLengths; + | forall2 _ _ _ = raise ListPair.UnequalLengths; -fun map_split f [] = ([], []) +fun map_split _ [] = ([], []) | map_split f (x :: xs) = let val (y, w) = f x;