1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Nov 23 13:45:16 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Nov 23 14:34:05 2009 +0100
     1.3 @@ -1370,10 +1370,10 @@
     1.4                    u1 u2
     1.5        | Op2 (Composition, _, R, u1, u2) =>
     1.6          let
     1.7 -          val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u2))
     1.8 -          val (_, c_T) = HOLogic.dest_prodT (domain_type (type_of u1))
     1.9 -          val ab_k = card_of_domain_from_rep 2 (rep_of u2)
    1.10 -          val bc_k = card_of_domain_from_rep 2 (rep_of u1)
    1.11 +          val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u1))
    1.12 +          val (_, c_T) = HOLogic.dest_prodT (domain_type (type_of u2))
    1.13 +          val ab_k = card_of_domain_from_rep 2 (rep_of u1)
    1.14 +          val bc_k = card_of_domain_from_rep 2 (rep_of u2)
    1.15            val ac_k = card_of_domain_from_rep 2 R
    1.16            val a_k = exact_root 2 (ac_k * ab_k div bc_k)
    1.17            val b_k = exact_root 2 (ab_k * bc_k div ac_k)
    1.18 @@ -1385,8 +1385,8 @@
    1.19          in
    1.20            (case body_R of
    1.21               Formula Neut =>
    1.22 -             kk_join (to_rep (Func (Struct [a_R, b_R], Formula Neut)) u2)
    1.23 -                     (to_rep (Func (Struct [b_R, c_R], Formula Neut)) u1)
    1.24 +             kk_join (to_rep (Func (Struct [a_R, b_R], Formula Neut)) u1)
    1.25 +                     (to_rep (Func (Struct [b_R, c_R], Formula Neut)) u2)
    1.26             | Opt (Atom (2, _)) =>
    1.27               let
    1.28                 (* Kodkod.rel_expr -> rep -> rep -> nut -> Kodkod.rel_expr *)
    1.29 @@ -1394,8 +1394,8 @@
    1.30                   kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) r
    1.31                 (* Kodkod.rel_expr -> Kodkod.rel_expr *)
    1.32                 fun do_term r =
    1.33 -                 kk_product (kk_join (do_nut r a_R b_R u2)
    1.34 -                                     (do_nut r b_R c_R u1)) r
    1.35 +                 kk_product (kk_join (do_nut r a_R b_R u1)
    1.36 +                                     (do_nut r b_R c_R u2)) r
    1.37               in kk_union (do_term true_atom) (do_term false_atom) end
    1.38             | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
    1.39            |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))