1.1 --- a/src/HOL/Tools/refute.ML	Wed Oct 21 16:54:04 2009 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Oct 21 16:57:57 2009 +0200
     1.3 @@ -1081,7 +1081,7 @@
     1.4        | next max len sum (x1::x2::xs) =
     1.5        if x1>0 andalso (x2<max orelse max<0) then
     1.6          (* we can shift *)
     1.7 -        SOME (valOf (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
     1.8 +        SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
     1.9        else
    1.10          (* continue search *)
    1.11          next max (len+1) (sum+x1) (x2::xs)
    1.12 @@ -1158,7 +1158,7 @@
    1.13        val axioms = collect_axioms thy u
    1.14        (* Term.typ list *)
    1.15        val types = Library.foldl (fn (acc, t') =>
    1.16 -        acc union (ground_types thy t')) ([], u :: axioms)
    1.17 +        uncurry (union (op =)) (acc, (ground_types thy t'))) ([], u :: axioms)
    1.18        val _     = tracing ("Ground types: "
    1.19          ^ (if null types then "none."
    1.20             else commas (map (Syntax.string_of_typ_global thy) types)))
    1.21 @@ -1620,30 +1620,14 @@
    1.22    end;
    1.23  
    1.24  (* ------------------------------------------------------------------------- *)
    1.25 -(* sum: returns the sum of a list 'xs' of integers                           *)
    1.26 -(* ------------------------------------------------------------------------- *)
    1.27 -
    1.28 -  (* int list -> int *)
    1.29 -
    1.30 -  fun sum xs = List.foldl op+ 0 xs;
    1.31 -
    1.32 -(* ------------------------------------------------------------------------- *)
    1.33 -(* product: returns the product of a list 'xs' of integers                   *)
    1.34 -(* ------------------------------------------------------------------------- *)
    1.35 -
    1.36 -  (* int list -> int *)
    1.37 -
    1.38 -  fun product xs = List.foldl op* 1 xs;
    1.39 -
    1.40 -(* ------------------------------------------------------------------------- *)
    1.41  (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
    1.42  (*               is the sum (over its constructors) of the product (over     *)
    1.43  (*               their arguments) of the size of the argument types          *)
    1.44  (* ------------------------------------------------------------------------- *)
    1.45  
    1.46    fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
    1.47 -    sum (map (fn (_, dtyps) =>
    1.48 -      product (map (size_of_type thy (typ_sizes, []) o
    1.49 +    Integer.sum (map (fn (_, dtyps) =>
    1.50 +      Integer.prod (map (size_of_type thy (typ_sizes, []) o
    1.51          (typ_of_dtyp descr typ_assoc)) dtyps))
    1.52            constructors);
    1.53  
    1.54 @@ -2330,8 +2314,8 @@
    1.55              let
    1.56                (* number of all constructors, including those of different  *)
    1.57                (* (mutually recursive) datatypes within the same descriptor *)
    1.58 -              val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs)
    1.59 -                (#descr info))
    1.60 +              val mconstrs_count =
    1.61 +                Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info))
    1.62              in
    1.63                if mconstrs_count < length params then
    1.64                  (* too many actual parameters; for now we'll use the *)
    1.65 @@ -2435,7 +2419,7 @@
    1.66                        (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
    1.67                    (* sanity check: typ_assoc must associate types to the   *)
    1.68                    (*               elements of 'dtyps' (and only to those) *)
    1.69 -                  val _ = if not (Library.eq_set (dtyps, map fst typ_assoc))
    1.70 +                  val _ = if not (eq_set (op =) (dtyps, map fst typ_assoc))
    1.71                      then
    1.72                        raise REFUTE ("IDT_recursion_interpreter",
    1.73                          "type association has extra/missing elements")
    1.74 @@ -3027,7 +3011,7 @@
    1.75          [Type ("fun", [T, Type ("bool", [])]),
    1.76           Type ("fun", [_, Type ("bool", [])])]),
    1.77           Type ("fun", [_, Type ("bool", [])])])) =>
    1.78 -      let nonfix union (* because "union" is used below *)
    1.79 +      let
    1.80          val size_elem = size_of_type thy model T
    1.81          (* the universe (i.e. the set that contains every element) *)
    1.82          val i_univ = Node (replicate size_elem TT)