# HG changeset patch
# User wenzelm
# Date 997285172 -7200
# Node ID 085a0d2857e84fb2c0ae117adf794a4c10ffb089
# Parent  f9ae28f55178964fc726cae0bbeb976f5dbe09d7
added constify_ast_tr;

diff -r f9ae28f55178 -r 085a0d2857e8 src/Pure/Syntax/syn_trans.ML
--- 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,