--- 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,