--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Mar 30 12:07:31 2019 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Mar 30 20:54:47 2019 +0100
@@ -973,7 +973,7 @@
\because their proofs contain oracles:" proved'));
val prv_path = Path.ext "prv" path;
val _ =
- Export.export thy prv_path
+ Export.export thy (Path.binding (prv_path, Position.none))
[implode (map (fn (s, _) => snd (strip_number s) ^
" -- proved by " ^ Distribution.version ^ "\n") proved'')];
in {pfuns = pfuns, type_map = type_map, env = NONE} end))