src/Pure/Syntax/syntax_trans.ML
changeset 46236 ae79f2978a67
parent 45389 bc0d50f8ae19
child 49660 de49d9b4d7bc
--- a/src/Pure/Syntax/syntax_trans.ML	Mon Jan 16 20:32:33 2012 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon Jan 16 21:50:15 2012 +0100
@@ -93,7 +93,9 @@
 
 (* constify *)
 
-fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
+fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] =
+      Ast.Appl [c, constify_ast_tr [ast1], ast2]
+  | constify_ast_tr [Ast.Variable c] = Ast.Constant c
   | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);