1.1 --- a/src/Pure/library.ML	Tue Jul 10 23:29:38 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jul 10 23:29:41 2007 +0200
     1.3 @@ -267,10 +267,8 @@
     1.4  fun (f oooo g) x y z w = f (g x y z w);
     1.5  
     1.6  (*function exponentiation: f(...(f x)...) with n applications of f*)
     1.7 -fun funpow n f x =
     1.8 -  let fun rep (0, x) = x
     1.9 -        | rep (n, x) = rep (n - 1, f x)
    1.10 -  in rep (n, x) end;
    1.11 +fun funpow 0 _ x = x
    1.12 +  | funpow n f x = funpow (n - 1) f (f x);
    1.13  
    1.14  
    1.15  (* exceptions *)
    1.16 @@ -750,7 +748,7 @@
    1.17        | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
    1.18        | untab pos ("\t" :: xs) ys =
    1.19            let val d = tab_width - (pos mod tab_width)
    1.20 -          in untab (pos + d) xs (replicate d " " @ ys) end
    1.21 +          in untab (pos + d) xs (funpow d (cons " ") ys) end
    1.22        | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
    1.23    in
    1.24      if not (exists (fn c => c = "\t") chs) then chs