summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/library.ML

changeset 46838 | c54b81bb9588 |

parent 46779 | 4f298836018b |

child 46891 | af4c1dd3963f |

equal
deleted
inserted
replaced

46837:5bdd68f380b3 | 46838:c54b81bb9588 |
---|---|

468 |
468 |

469 fun get_index f = |
469 fun get_index f = |

470 let |
470 let |

471 fun get (_: int) [] = NONE |
471 fun get (_: int) [] = NONE |

472 | get i (x :: xs) = |
472 | get i (x :: xs) = |

473 case f x |
473 (case f x of |

474 of NONE => get (i + 1) xs |
474 NONE => get (i + 1) xs |

475 | SOME y => SOME (i, y) |
475 | SOME y => SOME (i, y)) |

476 in get 0 end; |
476 in get 0 end; |

477 |
477 |

478 val flat = List.concat; |
478 val flat = List.concat; |

479 |
479 |

480 fun unflat (xs :: xss) ys = |
480 fun unflat (xs :: xss) ys = |