src/Pure/library.ML
changeset 47060 e2741ec9ae36
parent 47023 c7a89ecbc71e
child 47499 4b0daca2bf88
     1.1 --- a/src/Pure/library.ML	Tue Mar 20 21:37:31 2012 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Mar 21 11:00:34 2012 +0100
     1.3 @@ -328,7 +328,7 @@
     1.4  fun single x = [x];
     1.5  
     1.6  fun the_single [x] = x
     1.7 -  | the_single _ = raise Empty;
     1.8 +  | the_single _ = raise List.Empty;
     1.9  
    1.10  fun singleton f x = the_single (f [x]);
    1.11  
    1.12 @@ -372,12 +372,12 @@
    1.13  
    1.14  (*  (op @) [x1, ..., xn]  ===>  ((x1 @ x2) @ x3) ... @ xn
    1.15      for operators that associate to the left (TAIL RECURSIVE)*)
    1.16 -fun foldl1 f [] = raise Empty
    1.17 +fun foldl1 f [] = raise List.Empty
    1.18    | foldl1 f (x :: xs) = foldl f (x, xs);
    1.19  
    1.20  (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
    1.21      for n > 0, operators that associate to the right (not tail recursive)*)
    1.22 -fun foldr1 f [] = raise Empty
    1.23 +fun foldr1 f [] = raise List.Empty
    1.24    | foldr1 f l =
    1.25        let fun itr [x] = x
    1.26              | itr (x::l) = f(x, itr l)
    1.27 @@ -454,7 +454,7 @@
    1.28    in mapp 0 end;
    1.29  
    1.30  (*rear decomposition*)
    1.31 -fun split_last [] = raise Empty
    1.32 +fun split_last [] = raise List.Empty
    1.33    | split_last [x] = ([], x)
    1.34    | split_last (x :: xs) = apfst (cons x) (split_last xs);
    1.35