# HG changeset patch
# User blanchet
# Date 1280911864 -7200
# Node ID deaef70a8c058b75fa94f8912fcc65bced474c59
# Parent  b02e204b613a929f4d9ecf483c2f37ab8b9bc0ad
make SML/NJ happy

diff -r b02e204b613a -r deaef70a8c05 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Aug 04 10:39:35 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Aug 04 10:51:04 2010 +0200
@@ -797,10 +797,9 @@
 fun sym_break_axioms_for_constr_pair hol_ctxt binarize
        (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset,
                kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes
-       (constr1 as {const = const1 as (_, T1), delta = delta1,
-                    epsilon = epsilon1, ...},
-        constr2 as {const = const2 as (_, T2), delta = delta2,
-                    epsilon = epsilon2, ...}) =
+       (({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
+         {const = const2 as (_, T2), delta = delta2, epsilon = epsilon2, ...})
+        : constr_spec * constr_spec) =
   let
     val dataT = body_type T1
     val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these