src/Pure/Syntax/syntax_trans.ML
changeset 46236 ae79f2978a67
parent 45389 bc0d50f8ae19
child 49660 de49d9b4d7bc
equal deleted inserted replaced
46235:e4e0b5190f3d 46236:ae79f2978a67
    91   | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
    91   | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
    92 
    92 
    93 
    93 
    94 (* constify *)
    94 (* constify *)
    95 
    95 
    96 fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
    96 fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] =
       
    97       Ast.Appl [c, constify_ast_tr [ast1], ast2]
       
    98   | constify_ast_tr [Ast.Variable c] = Ast.Constant c
    97   | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
    99   | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
    98 
   100 
    99 
   101 
   100 (* type syntax *)
   102 (* type syntax *)
   101 
   103