author | wenzelm |
Thu, 31 Jan 2019 16:32:41 +0100 | |
changeset 69769 | c19a32cb9625 |
parent 69767 | d10fafeb93c0 |
child 69770 | efb0e5332441 |
--- a/src/Pure/library.ML Thu Jan 31 09:30:15 2019 +0100 +++ b/src/Pure/library.ML Thu Jan 31 16:32:41 2019 +0100 @@ -251,8 +251,8 @@ fun (f oooo g) x y z w = f (g x y z w); (*function exponentiation: f (... (f x) ...) with n applications of f*) -fun funpow (0 : int) _ = I - | funpow n f = f #> funpow (n - 1) f; +fun funpow (0: int) _ x = x + | funpow n f x = funpow (n - 1) f (f x); fun funpow_yield (0 : int) _ x = ([], x) | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;