# HG changeset patch
# User nipkow
# Date 1708288503 -3600
# Node ID 0a152b2f73aebde32a06d9a7247046875506c871
# Parent  26fa2e8761fb517cc9e213563b18075de571bebc
time funs: +1 instead of 1+

diff -r 26fa2e8761fb -r 0a152b2f73ae src/HOL/Data_Structures/Define_Time_Function.ML
--- 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 =