--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Jan 03 18:33:17 2012 +0100
@@ -786,7 +786,7 @@
(to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
| Op2 (Subset, _, _, u1, u2) =>
let
- val dom_T = domain_type (type_of u1)
+ val dom_T = elem_type (type_of u1)
val R1 = rep_of u1
val R2 = rep_of u2
val (dom_R, ran_R) =
@@ -1060,7 +1060,7 @@
| Op1 (Finite, _, Opt (Atom _), _) => KK.None
| Op1 (Converse, T, R, u1) =>
let
- val (b_T, a_T) = HOLogic.dest_prodT (domain_type T)
+ val (b_T, a_T) = HOLogic.dest_prodT (elem_type T)
val (b_R, a_R) =
case R of
Func (Struct [R1, R2], _) => (R1, R2)
@@ -1191,8 +1191,8 @@
end
| Op2 (Composition, _, R, u1, u2) =>
let
- val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u1))
- val (_, c_T) = HOLogic.dest_prodT (domain_type (type_of u2))
+ val (a_T, b_T) = HOLogic.dest_prodT (elem_type (type_of u1))
+ val (_, c_T) = HOLogic.dest_prodT (elem_type (type_of u2))
val ab_k = card_of_domain_from_rep 2 (rep_of u1)
val bc_k = card_of_domain_from_rep 2 (rep_of u2)
val ac_k = card_of_domain_from_rep 2 R