# 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 ::;