diff -r 24fb44c1086a -r c37a1f29bbc0 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Jul 08 14:37:19 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Jul 08 15:17:40 2011 +0200
@@ -886,7 +886,7 @@
            (proved, []) =>
              (Thm.join_proofs (maps (the o #2 o snd) proved);
               File.write (Path.ext "prv" path)
-                (concat (map (fn (s, _) => snd (strip_number s) ^
+                (implode (map (fn (s, _) => snd (strip_number s) ^
                    " -- proved by " ^ Distribution.version ^ "\n") proved));
               {pfuns = pfuns, type_map = type_map, env = NONE})
          | (_, unproved) => err_vcs (map fst unproved))