diff -r 843dba3d307a -r c007e6d9941d src/HOL/HOLCF/IOA/Sequence.thy --- a/src/HOL/HOLCF/IOA/Sequence.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/HOLCF/IOA/Sequence.thy Tue Oct 01 20:39:16 2024 +0200 @@ -72,8 +72,6 @@ syntax "_totlist" :: "args \ 'a Seq" (\(\indent=1 notation=\mixfix total list enumeration\\[_!])\) "_partlist" :: "args \ 'a Seq" (\(\indent=1 notation=\mixfix partial list enumeration\\[_?])\) -syntax_consts - Consq translations "[x, xs!]" \ "x \ [xs!]" "[x!]" \ "x\nil"