--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Dec 07 11:56:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Dec 07 11:56:01 2010 +0100
@@ -1510,33 +1510,6 @@
| _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
|> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
end
- | Op2 (Image, T, R, u1, u2) =>
- (case (rep_of u1, rep_of u2) of
- (Func (R11, R12), Func (R21, Formula Neut)) =>
- if R21 = R11 andalso is_lone_rep R12 then
- let
- fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)
- val core_r = big_join (to_r u2)
- val core_R = Func (R12, Formula Neut)
- in
- if is_opt_rep R12 then
- let
- val schema = atom_schema_of_rep R21
- val decls = decls_for_atom_schema ~1 schema
- val vars = unary_var_seq ~1 (length decls)
- val f = kk_some (big_join (fold1 kk_product vars))
- in
- kk_rel_if (kk_all decls f)
- (rel_expr_from_rel_expr kk R core_R core_r)
- (rel_expr_from_rel_expr kk R (opt_rep ofs T core_R)
- (kk_product core_r true_atom))
- end
- else
- rel_expr_from_rel_expr kk R core_R core_r
- end
- else
- raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])
- | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))
| Op2 (Apply, @{typ nat}, _,
Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then