diff -r c2535056434f -r 1eddc169baea src/HOL/Data_Structures/Define_Time_Function.ML
--- a/src/HOL/Data_Structures/Define_Time_Function.ML	Thu Oct 31 09:24:10 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML	Thu Oct 31 15:46:33 2024 +0100
@@ -222,7 +222,6 @@
 }
 
 (* Walks over term and calls given converter *)
-(* get rid and use Term.strip_abs.eta especially for lambdas *)
 fun list_abs ([], t) = t
   | list_abs (a::abs,t) = list_abs (abs,t) |> absfree a
 fun walk ctxt (origin: term list) (conv as {ifc, casec, funcc, letc, ...} : 'a converter) (t as _ $ _) =
@@ -263,19 +262,17 @@
 fun freeTypes (TVar ((t, _), T)) = TFree (t, T)
   | freeTypes t = t
 
-fun noFun (Type ("fun", _)) = error "Functions in datatypes are not allowed in case constructions"
-  | noFun T = T
-fun casecBuildBounds n t = if n > 0 then casecBuildBounds (n-1) (t $ (Bound (n-1))) else t
-fun casecAbs wctxt n (Type ("fun",[T,Tr])) (Abs (v,Ta,t)) = (map_atyps noFun T; Abs (v,Ta,casecAbs wctxt n Tr t))
-  | casecAbs wctxt n (Type ("fun",[T,Tr])) t =
-    (map_atyps noFun T; Abs ("uu",T,casecAbs wctxt (n + 1) Tr t))
-  | casecAbs wctxt n _ t = (#f wctxt) (casecBuildBounds n (Term.incr_bv n 0 t))
-fun fixCasecCases _ _ [t] = [t]
-  | fixCasecCases wctxt (Type (_,[T,Tr])) (t::ts) = casecAbs wctxt 0 T t :: fixCasecCases wctxt Tr ts
-  | fixCasecCases _ _ _ = error "Internal error: invalid case types/terms"
-fun fixCasec wctxt (t as Const (_,T)) args =
-      (check_args "cases" (t,args); list_comb (t,fixCasecCases wctxt T args))
-  | fixCasec _ _ _ = error "Internal error: invalid case term"
+fun fixCasecCases _ [t] = [t]
+  | fixCasecCases wctxt (t::ts) =
+    let
+      val num = fastype_of t |> strip_type |> fst |> length
+      val c' = Term.strip_abs_eta num t |> list_abs
+    in
+      c' :: fixCasecCases wctxt ts
+    end
+  | fixCasecCases _ _ = error "Internal error: invalid case types/terms"
+fun fixCasec wctxt t args =
+      (check_args "cases" (t,args); list_comb (t,fixCasecCases wctxt args))
 
 fun shortFunc fixedNum (Const (nm,T)) = 
     Const (nm,T |> strip_type |>> drop fixedNum |> (op --->))
@@ -285,7 +282,6 @@
 fun shortOriginFunc (term: term list) fixedNum (f as (c as Const (_,_), _))  =
   if contains' const_comp term c then shortApp fixedNum f else f
   | shortOriginFunc _ _ t = t
-val _ = strip_abs
 fun map_abs f (t as Abs _) = t |> strip_abs ||> f |> list_abs
   | map_abs _ t = t
 fun fixTerms ctxt (term: term list) (fixedNum: int) (t as pT $ (eq $ l $ r)) =
@@ -414,11 +410,12 @@
 fun casecTyp (Type (n, [T1, T2])) =
       Type (n, [change_typ T1, (if casecIsCase T2 then casecTyp else casecLastTyp) T2])
   | casecTyp _ = error "Internal error: Invalid case type"
-fun casecAbs f (Abs (v,Ta,t)) = (case casecAbs f t of (nconst,t) => (nconst,Abs (v,Ta,t)))
+fun casecAbs f (Abs (v,Ta,t)) = (case casecAbs f (subst_bound (Free (v,Ta), t))
+                                  of (nconst,t) => (nconst,absfree (v,Ta) t))
   | casecAbs f t = (case f t of NONE => (false,HOLogic.zero) | SOME t => (true,t))
 fun casecArgs _ [t] = (false, [map_aterms use_origin t])
   | casecArgs f (t::ar) =
-    (case casecAbs f t of (nconst, tt) => 
+    (case casecAbs f t of (nconst, tt) =>
       casecArgs f ar ||> (fn ar => tt :: ar) |>> (if nconst then K true else I))
   | casecArgs _ _ = error "Internal error: Invalid case term"
 fun casec wctxt (Const (t,T)) args =
@@ -456,9 +453,9 @@
          then
           let
             val exp' = letc_lambda wctxt expT exp
-            val t' = list_abs ([(nm,type_of exp')], t')
+            val t' = list_abs ([(nm,fastype_of exp')], t')
           in
-            Const (@{const_name "HOL.Let"}, [type_of exp', type_of t'] ---> HOLogic.natT) $ exp' $ t'
+            Const (@{const_name "HOL.Let"}, [fastype_of exp', fastype_of t'] ---> HOLogic.natT) $ exp' $ t'
           end
          else t') |> SOME
       | NONE => NONE)
@@ -746,7 +743,6 @@
     val fixedFrees = (hd term) |> strip_comb |> snd |> take fixedNum 
     val fixedFreesNames = map (fst o dest_Free) fixedFrees
     val term = map (shortFunc fixedNum o fst o strip_comb) term
-
     fun correctTerm term =
     let
       val get_f = fst o strip_comb o get_l