# HG changeset patch
# User haftmann
# Date 1743801138 -7200
# Node ID 6d0bb38873976cdbd5c490a5d10cd737cebe6fd6
# Parent  8f6dc8483b1a78e679549dbe798b1faa419887b5
tuned

diff -r 8f6dc8483b1a -r 6d0bb3887397 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Apr 04 22:20:30 2025 +0200
+++ b/src/Tools/nbe.ML	Fri Apr 04 23:12:18 2025 +0200
@@ -380,11 +380,11 @@
       (fun_ident i sym,
         [([ml_list (rev (dict_params @ default_params))], apply_constr sym (dict_params @ default_params))]);
 
-    fun assemble_value_equation sym dict_params (([], args), rhs) =
+    fun assemble_value_eqn sym dict_params (([], args), rhs) =
       (fun_ident 0 sym, [([ml_list (rev (dict_params @ assemble_args args))], assemble_rhs NONE rhs)]);
 
     fun assemble_eqns (sym, (num_args, (dict_params, eqns, default_params))) =
-      (if Code_Symbol.is_value sym then [assemble_value_equation sym dict_params (the_single eqns)]
+      (if Code_Symbol.is_value sym then [assemble_value_eqn sym dict_params (the_single eqns)]
       else map_index (assemble_eqn sym dict_params default_params) eqns
         @ [assemble_default_eqn sym dict_params default_params (length eqns)],
       nbe_abss num_args (fun_ident 0 sym));
@@ -509,7 +509,7 @@
     |> (fn t => apps t (rev dict_frees))
   end;
 
-fun reconstruct_term ctxt (const_tab : Code_Symbol.T Inttab.table) t =
+fun reconstruct_term ctxt const_tab t =
   let
     fun take_until f [] = []
       | take_until f (x :: xs) = if f x then [] else x :: take_until f xs;