diff -r 20d7631b37d7 -r 8635ed5e4613 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sun Oct 20 13:41:56 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Sun Oct 20 15:37:19 2024 +0200
@@ -11,6 +11,7 @@
     Variable of string |
     Appl of ast list
   val mk_appl: ast -> ast list -> ast
+  val constrain: ast -> ast -> ast
   exception AST of string * ast list
   val ast_ord: ast ord
   structure Table: TABLE
@@ -52,6 +53,8 @@
 fun mk_appl f [] = f
   | mk_appl f args = Appl (f :: args);
 
+fun constrain a b = Appl [Constant "_constrain", a, b];
+
 (*exception for system errors involving asts*)
 exception AST of string * ast list;