src/HOL/Option.thy

--- a/src/HOL/Option.thy	Tue Jan 12 13:36:01 2010 +0100
+++ b/src/HOL/Option.thy	Wed Jan 13 08:56:15 2010 +0100
@@ -115,11 +115,13 @@
   (SML "_ option")
   (OCaml "_ option")
   (Haskell "Maybe _")
+  (Scala "!Option[(_)]")
 
 code_const None and Some
   (SML "NONE" and "SOME")
   (OCaml "None" and "Some _")
   (Haskell "Nothing" and "Just")
+  (Scala "None" and "!Some((_))")
 
 code_instance option :: eq
   (Haskell -)
@@ -133,4 +135,7 @@
 code_reserved OCaml
   option None Some
 
+code_reserved Scala
+  Option None Some
+
 end