| changeset 81590 | e656c5edc352 |
| parent 80661 | 231d58c412b5 |
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sat Dec 14 16:58:53 2024 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sat Dec 14 17:35:53 2024 +0100 @@ -488,7 +488,7 @@ Syntax.Parse_Rule (case_trans true false) :: abscon_trans false @ abscon_trans true in - val thy = Sign.add_trrules trans_rules thy + val thy = Sign.translations_global true trans_rules thy end (* prove beta reduction rule for case combinator *)