# HG changeset patch
# User wenzelm
# Date 1321706198 -3600
# Node ID a6d9464a230bc7249b28dea933754c592f13f010
# Parent  41a768a431a60cf8cfc5b041f712d17037dbb1ee
discontinued slightly odd write_prv, which would still write .prv files the first time, and deprive add-on tools from date stamp change (cf. 157e74588c49);

diff -r 41a768a431a6 -r a6d9464a230b src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 19 13:02:50 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Nov 19 13:36:38 2011 +0100
@@ -880,10 +880,6 @@
          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
@@ -892,7 +888,7 @@
              (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
            (proved, []) =>
              (Thm.join_proofs (maps (the o #2 o snd) proved);
-              write_prv path
+              File.write (Path.ext "prv" path)
                 (implode (map (fn (s, _) => snd (strip_number s) ^
                    " -- proved by " ^ Distribution.version ^ "\n") proved));
               {pfuns = pfuns, type_map = type_map, env = NONE})