# HG changeset patch
# User haftmann
# Date 1744654745 -7200
# Node ID 38550f21275d0fec1685dd1d3084502dc98ad154
# Parent  289b189559602a9b00b7a04cf63a58494f2826e8
tuned

diff -r 289b18955960 -r 38550f21275d src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Apr 14 20:19:05 2025 +0200
+++ b/src/Tools/nbe.ML	Mon Apr 14 20:19:05 2025 +0200
@@ -341,10 +341,11 @@
 
 fun assemble_preprocessed_eqnss ctxt idx_of_sym deps eqnss =
   let
-    fun fun_ident sym = space_implode "_"
-      ["c", if Code_Symbol.is_value sym then "value" else string_of_int (idx_of_sym sym), Code_Symbol.default_base sym, "nbe"];
-    fun seq_fun_ident i sym = space_implode "_"
-      ["c", string_of_int (idx_of_sym sym), Code_Symbol.default_base sym, string_of_int i];
+    fun suffixed_fun_ident suffix sym = space_implode "_"
+      ["c", if Code_Symbol.is_value sym then "value" else string_of_int (idx_of_sym sym),
+      Code_Symbol.default_base sym, suffix];
+    val fun_ident = suffixed_fun_ident "nbe";
+    fun seq_fun_ident i = suffixed_fun_ident (string_of_int i);
     fun constr_ident sym =
       if Config.get ctxt trace
       then string_of_int (idx_of_sym sym) ^ " (*" ^ Code_Symbol.default_base sym ^ "*)"
@@ -413,7 +414,7 @@
         (seq_fun_ident i sym, (a_args, a_rhs) :: fallback_eqn)
       end;
 
-    fun assemble_default_eqn sym a_tparams a_dict_params a_global_params i =
+    fun assemble_fallback_eqn sym a_tparams a_dict_params a_global_params i =
       (seq_fun_ident i sym,
         [(replicate (length a_global_params) "_", assemble_app_constr sym a_tparams (a_dict_params @ a_global_params))])
 
@@ -421,7 +422,7 @@
           assemble_rhs NONE rhs
       | assemble_seq_eqns sym a_tparams a_dict_params a_global_params eqns =
           ml_let (ml_fundefs (map_index (assemble_eqn sym a_global_params) eqns
-            @ [assemble_default_eqn sym a_tparams a_dict_params a_global_params (length eqns)]))
+            @ [assemble_fallback_eqn sym a_tparams a_dict_params a_global_params (length eqns)]))
           (assemble_app_seq_fun 0 sym a_global_params);
 
     fun assemble_eqns (sym, (num_args, (a_tparams, a_dict_params, a_global_params, eqns))) =