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