src/Pure/Syntax/syn_trans.ML

 struct
 
 
 (** parse (ast) translations **)
 
+(* constify *)
+
+fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
+  | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
+
+
 (* application *)
 
 fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
   | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
 

 
 
 (** pure_trfuns **)
 
 val pure_trfuns =
- ([("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
-   ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
-   ("_bigimpl", bigimpl_ast_tr)],
+ ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
+   ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)],
   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
   []: (string * (term list -> term)) list,
   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
    ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);