# HG changeset patch
# User haftmann
# Date 1743326492 -7200
# Node ID f0a8d882c03178850e757c75dfd51dec7387d290
# Parent  003bef1acb2c5980da46294c17c6af31da4dacb9
tuned

diff -r 003bef1acb2c -r f0a8d882c031 src/Tools/Code/code_thingol.ML
--- 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