--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sun Nov 06 16:29:22 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sun Nov 06 16:41:53 2011 +0100
@@ -880,6 +880,10 @@
prefix = prefix}}
| x => x);
+fun write_prv path s =
+ let val path_prv = Path.ext "prv" path;
+ in if try File.read path_prv = SOME s then () else File.write path_prv s end;
+
fun close thy =
thy |>
VCs.map (fn
@@ -888,7 +892,7 @@
(if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
(proved, []) =>
(Thm.join_proofs (maps (the o #2 o snd) proved);
- File.write (Path.ext "prv" path)
+ write_prv path
(implode (map (fn (s, _) => snd (strip_number s) ^
" -- proved by " ^ Distribution.version ^ "\n") proved));
{pfuns = pfuns, type_map = type_map, env = NONE})