tuned;
authorwenzelm
Sun, 20 Oct 2024 13:13:17 +0200
changeset 81207 00df78aa2b0c
parent 81206 f2265c6beb8a
child 81208 893b056542e7
tuned;
src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sat Oct 19 22:57:43 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Sun Oct 20 13:13:17 2024 +0200
@@ -144,9 +144,9 @@
   | unfold_ast _ y = [y];
 
 fun unfold_ast_p c (y as Appl [Appl [Constant "_constrain", Constant c', _], x, xs]) =
-      if c = c' then apfst (cons x) (unfold_ast_p c xs) else ([], y)
+      if c = c' then unfold_ast_p c xs |>> cons x else ([], y)
   | unfold_ast_p c (y as Appl [Constant c', x, xs]) =
-      if c = c' then apfst (cons x) (unfold_ast_p c xs) else ([], y)
+      if c = c' then unfold_ast_p c xs |>> cons x else ([], y)
   | unfold_ast_p _ y = ([], y);