--- a/src/Pure/Syntax/syn_trans.ML Wed Aug 08 17:39:16 2001 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Wed Aug 08 17:39:32 2001 +0200
@@ -51,6 +51,12 @@
(** 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)
@@ -337,9 +343,8 @@
(** 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,