diff -r cfe74b0eecb1 -r 628fee3eb449 doc-src/Codegen/Thy/examples/example.ML --- a/doc-src/Codegen/Thy/examples/example.ML Tue Aug 17 14:19:12 2010 +0200 +++ b/doc-src/Codegen/Thy/examples/example.ML Tue Aug 17 14:19:12 2010 +0200 @@ -1,5 +1,6 @@ structure Example : sig - val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a + val id : 'a -> 'a + val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b val rev : 'a list -> 'a list datatype 'a queue = AQueue of 'a list * 'a list val empty : 'a queue @@ -7,10 +8,12 @@ val enqueue : 'a -> 'a queue -> 'a queue end = struct -fun foldl f a [] = a - | foldl f a (x :: xs) = foldl f (f a x) xs; +fun id x = (fn xa => xa) x; -fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs; +fun fold f [] = id + | fold f (x :: xs) = fold f xs o f x; + +fun rev xs = fold (fn a => fn b => a :: b) xs []; datatype 'a queue = AQueue of 'a list * 'a list;