src/HOL/Tools/refute.ML
changeset 33037 b22e44496dc2
parent 33002 f3f02f36a3e2
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -1154,7 +1154,7 @@
     1.4        val axioms = collect_axioms thy u
     1.5        (* Term.typ list *)
     1.6        val types = Library.foldl (fn (acc, t') =>
     1.7 -        acc union (ground_types thy t')) ([], u :: axioms)
     1.8 +        gen_union (op =) (acc, (ground_types thy t'))) ([], u :: axioms)
     1.9        val _     = tracing ("Ground types: "
    1.10          ^ (if null types then "none."
    1.11             else commas (map (Syntax.string_of_typ_global thy) types)))
    1.12 @@ -2415,7 +2415,7 @@
    1.13                        (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
    1.14                    (* sanity check: typ_assoc must associate types to the   *)
    1.15                    (*               elements of 'dtyps' (and only to those) *)
    1.16 -                  val _ = if not (Library.eq_set (dtyps, map fst typ_assoc))
    1.17 +                  val _ = if not (gen_eq_set (op =) (dtyps, map fst typ_assoc))
    1.18                      then
    1.19                        raise REFUTE ("IDT_recursion_interpreter",
    1.20                          "type association has extra/missing elements")
    1.21 @@ -3007,7 +3007,7 @@
    1.22          [Type ("fun", [T, Type ("bool", [])]),
    1.23           Type ("fun", [_, Type ("bool", [])])]),
    1.24           Type ("fun", [_, Type ("bool", [])])])) =>
    1.25 -      let nonfix union (* because "union" is used below *)
    1.26 +      let
    1.27          val size_elem = size_of_type thy model T
    1.28          (* the universe (i.e. the set that contains every element) *)
    1.29          val i_univ = Node (replicate size_elem TT)