--- 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 --| $$ "]"