# HG changeset patch
# User blanchet
# Date 1330597736 -3600
# Node ID 18ba7f63217d5bc03f33889afb07aeea58f2574a
# Parent  8e365bc843e9641ae7ef1f2120d3ceab22e46f56
more robust set element extractor

diff -r 8e365bc843e9 -r 18ba7f63217d src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Mar 01 10:12:58 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Mar 01 11:28:56 2012 +0100
@@ -1060,7 +1060,7 @@
       | Op1 (Finite, _, Opt (Atom _), _) => KK.None
       | Op1 (Converse, T, R, u1) =>
         let
-          val (b_T, a_T) = HOLogic.dest_prodT (elem_type T)
+          val (b_T, a_T) = HOLogic.dest_prodT (pseudo_domain_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 (elem_type (type_of u1))
-          val (_, c_T) = HOLogic.dest_prodT (elem_type (type_of u2))
+          val (a_T, b_T) = HOLogic.dest_prodT (pseudo_domain_type (type_of u1))
+          val (_, c_T) = HOLogic.dest_prodT (pseudo_domain_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