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 =