# HG changeset patch
# User blanchet
# Date 1280757152 -7200
# Node ID 346df80a092402ad7a37e499317f21091ad43283
# Parent  bc546396b818810e462d4490ebbaeee17b76af59
optimize generated Kodkod formula

diff -r bc546396b818 -r 346df80a0924 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Aug 02 14:27:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Aug 02 15:52:32 2010 +0200
@@ -436,13 +436,11 @@
   case arity_of_rep R1 of
     1 => kk_join r1 r2
   | arity1 =>
-    let
-      val unpacked_rs1 =
-        if inline_rel_expr r1 then unpack_vect_in_chunks kk 1 arity1 r1
-        else unpack_products r1
-    in
+    let val unpacked_rs1 = unpack_products r1 in
       if one andalso length unpacked_rs1 = arity1 then
         fold kk_join unpacked_rs1 r2
+      else if one andalso inline_rel_expr r1 then
+        fold kk_join (unpack_vect_in_chunks kk 1 arity1 r1) r2
       else
         kk_project_seq
             (kk_intersect (kk_product r1 (full_rel_for_rep res_R)) r2)