--- 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))