# HG changeset patch
# User wenzelm
# Date 1184102981 -7200
# Node ID 8ff68cb5860c72f94bac8ace394a4d95e236e7ee
# Parent  5104b2959ed0a88a864b7f307f93aee6bcecec24
simplified funpow, untabify;

diff -r 5104b2959ed0 -r 8ff68cb5860c src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jul 10 23:29:38 2007 +0200
+++ b/src/Pure/library.ML	Tue Jul 10 23:29:41 2007 +0200
@@ -267,10 +267,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 n f x =
-  let fun rep (0, x) = x
-        | rep (n, x) = rep (n - 1, f x)
-  in rep (n, x) end;
+fun funpow 0 _ x = x
+  | funpow n f x = funpow (n - 1) f (f x);
 
 
 (* exceptions *)
@@ -750,7 +748,7 @@
       | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
       | untab pos ("\t" :: xs) ys =
           let val d = tab_width - (pos mod tab_width)
-          in untab (pos + d) xs (replicate d " " @ ys) end
+          in untab (pos + d) xs (funpow d (cons " ") ys) end
       | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
   in
     if not (exists (fn c => c = "\t") chs) then chs