# HG changeset patch
# User blanchet
# Date 1280681869 -7200
# Node ID faa18bf13b9b4274654430d02f2f38b1b83ea575
# Parent  b730aac146127d78d8682f59e8accda4519cf1e8
fix bug with Kodkodi < 1.2.14

diff -r b730aac14612 -r faa18bf13b9b src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sun Aug 01 17:43:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sun Aug 01 18:57:49 2010 +0200
@@ -320,9 +320,8 @@
   case getenv "KODKODI_VERSION" of
     "" => false
   | s => dict_ord int_ord (s |> space_explode "."
-                             |> map (the o Int.fromString),
+                             |> map (the_default 0 o Int.fromString),
                            [1, 2, 13]) = GREATER
-         handle Option.Option => false
 
 (** Auxiliary functions on Kodkod problems **)
 
@@ -892,7 +891,7 @@
   >> (fn ((n, j), SOME _) => (n, ~j - 1)
        | ((n, j), NONE) => (n, if new_kodkodi then j
                                else if j mod 2 = 0 then j div 2
-                               else ~(j - 1) div 2))
+                               else ~(j + 1) div 2))
 val scan_atom = $$ "A" |-- scan_nat
 val scan_tuple = $$ "[" |-- scan_list scan_atom --| $$ "]"
 val scan_tuple_set = $$ "[" |-- scan_list scan_tuple --| $$ "]"