src/HOL/SPARK/Tools/spark_vcs.ML
changeset 69784 24bbc4e30e5b
parent 69099 d44cb8a3e5e0
child 70015 c8e08d8ffb93
     1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Feb 02 14:51:11 2019 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Feb 02 15:52:14 2019 +0100
     1.3 @@ -973,7 +973,7 @@
     1.4               \because their proofs contain oracles:" proved'));
     1.5            val prv_path = Path.ext "prv" path;
     1.6            val _ =
     1.7 -            Export.export thy (Path.implode prv_path)
     1.8 +            Export.export thy prv_path
     1.9                [implode (map (fn (s, _) => snd (strip_number s) ^
    1.10                  " -- proved by " ^ Distribution.version ^ "\n") proved'')];
    1.11          in {pfuns = pfuns, type_map = type_map, env = NONE} end))