--- a/src/HOL/Data_Structures/Define_Time_Function.ML Sun Feb 18 15:16:20 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Sun Feb 18 21:35:03 2024 +0100
@@ -360,7 +360,7 @@
casec = casec,
letc = letc
}
-fun top_converter is_rec _ _ = opt_term o (plus (if is_rec then SOME one else NONE))
+fun top_converter is_rec _ _ = opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE))
(* Use converter to convert right side of a term *)
fun to_time ctxt origin converter top_converter term =