diff -r 079fe4292526 -r c7723cc15de8 src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/Representable.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -32,6 +32,7 @@
   assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
 
 syntax "_LIFTDEFL" :: "type \<Rightarrow> logic"  ("(1LIFTDEFL/(1'(_')))")
+syntax_consts "_LIFTDEFL" \<rightleftharpoons> liftdefl
 translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
 
 definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
@@ -51,6 +52,7 @@
   assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))"
 
 syntax "_DEFL" :: "type \<Rightarrow> logic"  ("(1DEFL/(1'(_')))")
+syntax_consts "_DEFL" \<rightleftharpoons> defl
 translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
 
 instance "domain" \<subseteq> predomain