diff -r 25978a474603 -r ed766dfdd2f1 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 27 16:52:04 2024 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Nov 29 10:35:47 2024 +0100
@@ -2165,7 +2165,7 @@
 \<close>
 
     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
-      "every_snd s = SCons (shd s) (stl (stl s))"
+      "every_snd s = SCons (shd s) (every_snd (stl (stl s)))"
 
 text \<open>
 \noindent
@@ -2506,7 +2506,7 @@
 
     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
       "shd (every_snd s) = shd s"
-    | "stl (every_snd s) = stl (stl s)"
+    | "stl (every_snd s) = every_snd (stl (stl s))"
 
 text \<open>
 \noindent