changeset 81590 | e656c5edc352 |
parent 81507 | 08574da77b4a |
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Sat Dec 14 16:58:53 2024 +0100 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Sat Dec 14 17:35:53 2024 +0100 @@ -57,7 +57,7 @@ thy |> Sign.add_consts (normal_decls @ map #1 transformed_decls) |> Sign.syntax_global true Syntax.mode_default (map #2 transformed_decls) - |> Sign.add_trrules (maps #3 transformed_decls) + |> Sign.translations_global true (maps #3 transformed_decls) end val add_consts = gen_add_consts Sign.certify_typ