--- a/src/Tools/nbe.ML Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Tools/nbe.ML Fri Sep 20 14:28:13 2024 +0200
@@ -203,7 +203,7 @@
infix 9 `$` `$$`;
fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
fun e `$$` [] = e
- | e `$$` es = "(" ^ e ^ " " ^ space_implode " " es ^ ")";
+ | e `$$` es = "(" ^ e ^ " " ^ implode_space es ^ ")";
fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")";
fun ml_cases t cs =
@@ -224,7 +224,7 @@
let
fun fundef (name, eqs) =
let
- fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e
+ fun eqn (es, e) = name ^ " " ^ implode_space es ^ " = " ^ e
in space_implode "\n | " (map eqn eqs) end;
in
(prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss