1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     1.3 @@ -424,7 +424,6 @@
     1.4     (@{const_name converse}, 1),
     1.5     (@{const_name trancl}, 1),
     1.6     (@{const_name rel_comp}, 2),
     1.7 -   (@{const_name prod}, 2),
     1.8     (@{const_name image}, 2),
     1.9     (@{const_name finite}, 1),
    1.10     (@{const_name unknown}, 0),

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 11:56:01 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 11:56:01 2010 +0100
     2.3 @@ -1510,28 +1510,6 @@
     2.4             | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
     2.5            |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
     2.6          end
     2.7 -      | Op2 (Product, T, R, u1, u2) =>
     2.8 -        let
     2.9 -          val (a_T, b_T) = HOLogic.dest_prodT (domain_type T)
    2.10 -          val a_k = card_of_domain_from_rep 2 (rep_of u1)
    2.11 -          val b_k = card_of_domain_from_rep 2 (rep_of u2)
    2.12 -          val a_R = Atom (a_k, offset_of_type ofs a_T)
    2.13 -          val b_R = Atom (b_k, offset_of_type ofs b_T)
    2.14 -          val body_R = body_rep R
    2.15 -        in
    2.16 -          (case body_R of
    2.17 -             Formula Neut =>
    2.18 -             kk_product (to_rep (Func (a_R, Formula Neut)) u1)
    2.19 -                        (to_rep (Func (b_R, Formula Neut)) u2)
    2.20 -           | Opt (Atom (2, _)) =>
    2.21 -             let
    2.22 -               fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r
    2.23 -               fun do_term r =
    2.24 -                 kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
    2.25 -             in kk_union (do_term true_atom) (do_term false_atom) end
    2.26 -           | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u]))
    2.27 -          |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, b_R], body_R))
    2.28 -        end
    2.29        | Op2 (Image, T, R, u1, u2) =>
    2.30          (case (rep_of u1, rep_of u2) of
    2.31             (Func (R11, R12), Func (R21, Formula Neut)) =>

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:56:01 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:56:01 2010 +0100
     3.3 @@ -55,7 +55,6 @@
     3.4      Eq |
     3.5      Triad |
     3.6      Composition |
     3.7 -    Product |
     3.8      Image |
     3.9      Apply |
    3.10      Lambda
    3.11 @@ -170,7 +169,6 @@
    3.12    Eq |
    3.13    Triad |
    3.14    Composition |
    3.15 -  Product |
    3.16    Image |
    3.17    Apply |
    3.18    Lambda
    3.19 @@ -235,7 +233,6 @@
    3.20    | string_for_op2 Eq = "Eq"
    3.21    | string_for_op2 Triad = "Triad"
    3.22    | string_for_op2 Composition = "Composition"
    3.23 -  | string_for_op2 Product = "Product"
    3.24    | string_for_op2 Image = "Image"
    3.25    | string_for_op2 Apply = "Apply"
    3.26    | string_for_op2 Lambda = "Lambda"
    3.27 @@ -528,8 +525,6 @@
    3.28            Op1 (Closure, range_type T, Any, sub t1)
    3.29          | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
    3.30            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
    3.31 -        | (Const (@{const_name prod}, T), [t1, t2]) =>
    3.32 -          Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2)
    3.33          | (Const (@{const_name image}, T), [t1, t2]) =>
    3.34            Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    3.35          | (Const (x as (s as @{const_name Suc}, T)), []) =>