1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 19 13:02:50 2011 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 19 13:36:38 2011 +0100
     1.3 @@ -880,10 +880,6 @@
     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 @@ -892,7 +888,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 -              write_prv path
    1.19 +              File.write (Path.ext "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})