# HG changeset patch
# User blanchet
# Date 1284639843 -7200
# Node ID 37f1a961a91817ada3752ea2a7a699949ed0986e
# Parent  c6b21584f33641a2921b1c4f419a1c371a50c922
tuning

diff -r c6b21584f336 -r 37f1a961a918 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Thu Sep 16 13:52:17 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Thu Sep 16 14:24:03 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2008, 2009, 2010
 
-ML interface on top of Kodkod.
+ML interface for Kodkod.
 *)
 
 signature KODKOD =
diff -r c6b21584f336 -r 37f1a961a918 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Sep 16 13:52:17 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Sep 16 14:24:03 2010 +0200
@@ -1019,7 +1019,7 @@
 fun kodkod_formula_from_nut ofs
         (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
                 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
-                kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
+                kk_lone, kk_some, kk_rel_let, kk_rel_if, kk_union,
                 kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
                 kk_comprehension, kk_project, kk_project_seq, kk_not3,
                 kk_nat_less, kk_int_less, ...}) u =