--- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Apr 07 15:46:06 2021 +0000
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Apr 08 16:43:35 2021 +0200
@@ -975,8 +975,7 @@
Export.export thy (Path.binding (prv_path, Position.none))
(proved'' |> map (fn (s, _) =>
XML.Text (snd (strip_number s) ^
- " -- proved by Isabelle/" ^ Isabelle_System.isabelle_id () ^
- Isabelle_System.isabelle_heading () ^ "\n")));
+ " -- proved by " ^ Isabelle_System.identification () ^ "\n")));
in {pfuns = pfuns, type_map = type_map, env = NONE} end))
|> Sign.parent_path;