# HG changeset patch # User wenzelm # Date 1548948761 -3600 # Node ID c19a32cb96253d8fd909fe8d2a227d83584b9df9 # Parent d10fafeb93c0c08e12eee6b08183a430393a8e74 prefer tail-recursive version (despite 4b99b1214034); diff -r d10fafeb93c0 -r c19a32cb9625 src/Pure/library.ML --- 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 ::;