
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 \<Rightarrow> 'a Seq"  (\<open>(\<open>indent=1 notation=\<open>mixfix total list enumeration\<close>\<close>[_!])\<close>)
   "_partlist" :: "args \<Rightarrow> 'a Seq"  (\<open>(\<open>indent=1 notation=\<open>mixfix partial list enumeration\<close>\<close>[_?])\<close>)
-syntax_consts
-  Consq
 translations
   "[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
   "[x!]" \<rightleftharpoons> "x\<leadsto>nil"




