--- a/src/HOL/Library/code_test.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/HOL/Library/code_test.ML Tue Jan 03 16:05:07 2023 +0100
@@ -316,8 +316,8 @@
{environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE,
writeln = writeln, warning = warning}
Position.none
- (ML_Lex.read_text (code, Position.file (Path.implode_symbolic code_path)) @
- ML_Lex.read_text (driver, Position.file (Path.implode_symbolic driver_path)) @
+ (ML_Lex.read_text (code, Position.file (File.symbolic_path code_path)) @
+ ML_Lex.read_text (driver, Position.file (File.symbolic_path driver_path)) @
ML_Lex.read "main ()")
handle ERROR msg => error ("Evaluation for " ^ polymlN ^ " failed:\n" ^ msg)
in File.read out_path end