--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Nov 02 10:56:53 2019 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Nov 02 12:02:27 2019 +0100
@@ -973,8 +973,8 @@
val prv_path = Path.ext "prv" path;
val _ =
Export.export thy (Path.binding (prv_path, Position.none))
- [implode (map (fn (s, _) => snd (strip_number s) ^
- " -- proved by " ^ Distribution.version ^ "\n") proved'')];
+ (proved'' |> map (fn (s, _) =>
+ XML.Text (snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n")));
in {pfuns = pfuns, type_map = type_map, env = NONE} end))
|> Sign.parent_path;