# HG changeset patch
# User haftmann
# Date 1179424160 -7200
# Node ID d8b4f2dc2b1da6ecd9c9fb729025a34097d01def
# Parent  02440636214f8b67e693df17afa07559d93d3709
refined pow function

diff -r 02440636214f -r d8b4f2dc2b1d src/Pure/General/int.ML
--- a/src/Pure/General/int.ML	Thu May 17 19:49:17 2007 +0200
+++ b/src/Pure/General/int.ML	Thu May 17 19:49:20 2007 +0200
@@ -66,7 +66,16 @@
 nonfix div val div = curry div;
 nonfix mod val mod = curry mod;
 val neg = ~;
-val pow = fn k => fn l => pow (l, toInt k);
+
+fun pow k l =
+  let
+    fun pw 0 = 1
+      | pw k = mult l (pw (sub k 1));
+  in if k < zero
+    then error "pow: negative exponent"
+    else pw k
+  end;
+
 fun exp k = pow k two;
 val log = int o log2;