changeset 13073 | cc9d7f403a4b |
parent 13003 | 3d5807d45439 |
child 13731 | e2d17090052b |
--- a/src/Pure/codegen.ML Wed Mar 27 20:45:03 2002 +0100 +++ b/src/Pure/codegen.ML Thu Mar 28 16:28:12 2002 +0100 @@ -248,7 +248,9 @@ (if not (Symbol.is_letter x) then "id" else "") ^ check_str xs end; -val mk_const_id = gen_mk_id Sign.constK I; +val mk_const_id = gen_mk_id Sign.constK + (fn s => if s mem ThmDatabase.ml_reserved then s ^ "_const" else s); + val mk_type_id = gen_mk_id Sign.typeK (fn s => if s mem ThmDatabase.ml_reserved then s ^ "_type" else s);