1.1 --- a/src/HOL/Tools/refute.ML	Thu Sep 02 16:31:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Sep 02 16:45:21 2010 +0200
     1.3 @@ -1383,19 +1383,6 @@
     1.4    end;
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 -(* power: 'power (a, b)' computes a^b, for a>=0, b>=0                        *)
     1.8 -(* ------------------------------------------------------------------------- *)
     1.9 -
    1.10 -(* int * int -> int *)
    1.11 -
    1.12 -fun power (a, 0) = 1
    1.13 -  | power (a, 1) = a
    1.14 -  | power (a, b) =
    1.15 -      let val ab = power(a, b div 2) in
    1.16 -        ab * ab * power(a, b mod 2)
    1.17 -      end;
    1.18 -
    1.19 -(* ------------------------------------------------------------------------- *)
    1.20  (* size_of_type: returns the number of elements in a type 'T' (i.e. 'length  *)
    1.21  (*               (make_constants T)', but implemented more efficiently)      *)
    1.22  (* ------------------------------------------------------------------------- *)
    1.23 @@ -1415,7 +1402,7 @@
    1.24      (* returns the number of elements that have the same tree structure as a *)
    1.25      (* given interpretation                                                  *)
    1.26      fun size_of_intr (Leaf xs) = length xs
    1.27 -      | size_of_intr (Node xs) = power (size_of_intr (hd xs), length xs)
    1.28 +      | size_of_intr (Node xs) = Integer.pow (length xs) (size_of_intr (hd xs))
    1.29      (* obtain the interpretation for a variable of type 'T' *)
    1.30      val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1,
    1.31        bounds=[], wellformed=True} (Free ("dummy", T))
    1.32 @@ -2896,7 +2883,7 @@
    1.33              val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m)
    1.34              val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n)
    1.35              val len_elem = len_m + len_n
    1.36 -            val off_elem = off_m * power (size_elem, len_n) + off_n
    1.37 +            val off_elem = off_m * Integer.pow len_n size_elem + off_n
    1.38            in
    1.39              case AList.lookup op= lenoff'_lists (len_elem, off_elem) of
    1.40                NONE =>