diff -r 5b38730f3e12 -r cdff476ba39e src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Sep 02 16:31:50 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Sep 02 16:45:21 2010 +0200
@@ -1383,19 +1383,6 @@
   end;
 
 (* ------------------------------------------------------------------------- *)
-(* power: 'power (a, b)' computes a^b, for a>=0, b>=0                        *)
-(* ------------------------------------------------------------------------- *)
-
-(* int * int -> int *)
-
-fun power (a, 0) = 1
-  | power (a, 1) = a
-  | power (a, b) =
-      let val ab = power(a, b div 2) in
-        ab * ab * power(a, b mod 2)
-      end;
-
-(* ------------------------------------------------------------------------- *)
 (* size_of_type: returns the number of elements in a type 'T' (i.e. 'length  *)
 (*               (make_constants T)', but implemented more efficiently)      *)
 (* ------------------------------------------------------------------------- *)
@@ -1415,7 +1402,7 @@
     (* returns the number of elements that have the same tree structure as a *)
     (* given interpretation                                                  *)
     fun size_of_intr (Leaf xs) = length xs
-      | size_of_intr (Node xs) = power (size_of_intr (hd xs), length xs)
+      | size_of_intr (Node xs) = Integer.pow (length xs) (size_of_intr (hd xs))
     (* obtain the interpretation for a variable of type 'T' *)
     val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1,
       bounds=[], wellformed=True} (Free ("dummy", T))
@@ -2896,7 +2883,7 @@
             val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m)
             val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n)
             val len_elem = len_m + len_n
-            val off_elem = off_m * power (size_elem, len_n) + off_n
+            val off_elem = off_m * Integer.pow len_n size_elem + off_n
           in
             case AList.lookup op= lenoff'_lists (len_elem, off_elem) of
               NONE =>