--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Oct 27 22:34:37 2020 +0100
@@ -209,7 +209,7 @@
{line = 0, file = "generated code", verbose = verbose, debug = false} code)
fun with_overlord_dir name f =
- Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
+ (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
|> Isabelle_System.make_directory
|> Exn.capture f
|> Exn.release
@@ -258,7 +258,7 @@
[(narrowing_engine_file,
if contains_existentials then pnf_narrowing_engine else narrowing_engine),
(code_file, code), (main_file, main)])
- val executable = Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")
+ val executable = in_path + Path.basic "isabelle_quickcheck_narrowing"
val cmd =
"exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
(space_implode " "