--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Dec 14 16:58:53 2024 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Dec 14 17:35:53 2024 +0100
@@ -522,7 +522,7 @@
       val trans_rules : Ast.ast Syntax.trrule list =
           maps one_case_trans (pat_consts ~~ spec);
     in
-      val thy = Sign.add_trrules trans_rules thy;
+      val thy = Sign.translations_global true trans_rules thy;
     end;
 
     (* prove strictness and reduction rules of pattern combinators *)