src/HOL/Option.thy
changeset 81706 7beb0cf38292
parent 69275 9bbd5497befd
--- a/src/HOL/Option.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Option.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -373,13 +373,9 @@
 | constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
     (Haskell) infix 4 "=="
 
-code_reserved SML
-  option NONE SOME
-
-code_reserved OCaml
-  option None Some
-
-code_reserved Scala
-  Option None Some
+code_reserved
+  (SML) option NONE SOME
+  and (OCaml) option None Some
+  and (Scala) Option None Some
 
 end