diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Library/Option_ord.thy --- a/src/HOL/Library/Option_ord.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Library/Option_ord.thy Sat Oct 05 14:58:36 2024 +0200 @@ -449,6 +449,6 @@ instance option :: (complete_linorder) complete_linorder .. -unbundle no_lattice_syntax +unbundle no lattice_syntax end