src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
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 *)