# HG changeset patch
# User nipkow
# Date 1708770570 -3600
# Node ID 80cb54976c1c2c6cabb9fbd207524989026070bf
# Parent  d3a26436e679750301d0bcb8c1288ffcae1f7d22
timing function generation bug fix by Jonas Stahl

diff -r d3a26436e679 -r 80cb54976c1c src/HOL/Data_Structures/Define_Time_Function.ML
--- a/src/HOL/Data_Structures/Define_Time_Function.ML	Fri Feb 23 17:22:09 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML	Sat Feb 24 11:29:30 2024 +0100
@@ -205,9 +205,9 @@
 fun casecAbs ctxt f n (Type (_,[T,Tr])) (Abs (v,Ta,t)) = (noFun T; Abs (v,Ta,casecAbs ctxt f n Tr t))
   | casecAbs ctxt f n (Type (Tn,[T,Tr])) t =
     (noFun T; case Variable.variant_fixes ["x"] ctxt of ([v],ctxt) =>
-    (if Tn = "fun" then Abs(v,T,casecAbs ctxt f (n + 1) Tr t) else f t)
+    (if Tn = "fun" then Abs (v,T,casecAbs ctxt f (n + 1) Tr t) else f t)
     | _ => error "Internal error: could not fix variable")
-  | casecAbs _ f n _ t = f (casecBuildBounds n t)
+  | casecAbs _ f n _ t = f (casecBuildBounds n (Term.incr_bv n 0 t))
 fun fixCasecCases _ _ _ [t] = [t]
   | fixCasecCases ctxt f (Type (_,[T,Tr])) (t::ts) = casecAbs ctxt f 0 T t :: fixCasecCases ctxt f Tr ts
   | fixCasecCases _ _ _ _ = error "Internal error: invalid case types/terms"