src/HOL/HOLCF/Tools/cont_consts.ML
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