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 =>