--- a/src/Tools/Code/code_thingol.ML Fri Mar 28 14:13:40 2025 +0100
+++ b/src/Tools/Code/code_thingol.ML Sun Mar 30 11:21:32 2025 +0200
@@ -187,13 +187,13 @@
| _ => NONE);
val unfold_abs = unfoldr
- (fn (v `|=> (t, _)) => SOME (v, t)
+ (fn (v_ty `|=> (t, _)) => SOME (v_ty, t)
| _ => NONE);
-fun unfold_abs_typed (v_ty `|=> body) =
+fun unfold_abs_typed (v_ty `|=> t_ty) =
unfoldr
- (fn (v_ty `|=> body, _) => SOME (v_ty, body)
- | _ => NONE) body
+ (fn (v_ty `|=> t_ty, _) => SOME (v_ty, t_ty)
+ | _ => NONE) t_ty
|> apfst (cons v_ty)
|> SOME
| unfold_abs_typed _ = NONE