diff -r 6ddbfad8ca20 -r 406a85a25189 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Sep 20 14:28:13 2024 +0200
@@ -97,7 +97,7 @@
 fun run_compilation_text cookie ctxt comp vs_t args =
   let
     val (program_code, value_name) = comp vs_t;
-    val value_code = space_implode " "
+    val value_code = implode_space
       (value_name :: "()" :: map (enclose "(" ")") args);
   in Exn.result (value ctxt cookie) (program_code, value_code) end;
 
@@ -582,7 +582,7 @@
 
 fun print_computation kind ctxt T =
   print (fn { of_term_for_typ, ... } => fn prfx =>
-    enclose "(" ")" (space_implode " " [
+    enclose "(" ")" (implode_space [
       kind,
       "(Context.proof_of (Context.the_generic_context ()))",
       Long_Name.implode [prfx, generated_computationN, covered_constsN],
@@ -592,7 +592,7 @@
 
 fun print_computation_check ctxt =
   print (fn { of_term_for_typ, ... } => fn prfx =>
-    enclose "(" ")" (space_implode " " [
+    enclose "(" ")" (implode_space [
       mount_computation_checkN,
       "(Context.proof_of (Context.the_generic_context ()))",
       Long_Name.implode [prfx, generated_computationN, covered_constsN],