--- a/src/HOL/Limited_Sequence.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Limited_Sequence.thy Thu Jan 02 08:37:55 2025 +0100
@@ -200,8 +200,8 @@
end;
\<close>
-code_reserved Eval Limited_Sequence
-
+code_reserved
+ (Eval) Limited_Sequence
hide_const (open) yield empty single eval map_seq bind union if_seq not_seq map
pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
@@ -213,4 +213,3 @@
neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
end
-