--- a/src/HOL/Tools/Nitpick/kodkod.ML Fri Nov 05 19:39:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Fri Nov 05 19:47:20 2010 +0100
@@ -1085,15 +1085,15 @@
Normal (ps, js, first_error)
end
in remove_temporary_files (); outcome end
- handle Exn.Interrupt =>
+ handle Exn.Interrupt => (* FIXME Exn.is_interrupt *)
let
val nontriv_js =
read_output_file new_kodkodi out_path
|> snd |> snd |> map reindex
in
(remove_temporary_files ();
- Interrupted (SOME (triv_js @ nontriv_js)))
- handle Exn.Interrupt =>
+ Interrupted (SOME (triv_js @ nontriv_js))) (* FIXME violates Isabelle/ML exception model *)
+ handle Exn.Interrupt => (* FIXME violates Isabelle/ML exception model *)
(remove_temporary_files (); Interrupted NONE)
end
end