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