diff -r c2cca97a5797 -r a594d22e69d6 src/HOL/Data_Structures/Define_Time_Function.ML
--- a/src/HOL/Data_Structures/Define_Time_Function.ML	Mon Mar 25 17:55:02 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML	Wed Mar 27 16:48:23 2024 +0100
@@ -353,7 +353,9 @@
 
 (* The converter for timing functions given to the walker *)
 val converter : term option converter = {
-        constc = fn _ => fn _ => fn _ => fn _ => NONE,
+        constc = fn _ => fn _ => fn _ => fn t =>
+          (case t of Const ("HOL.undefined", _) => SOME (Const ("HOL.undefined", @{typ "nat"}))
+                   | _ => NONE),
         funcc = funcc,
         ifc = ifc,
         casec = casec,