src/HOL/Option.thy

--- a/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -8,7 +8,7 @@
 imports BNF_LFP Datatype Finite_Set
 begin
 
-datatype_new 'a option = None | Some 'a
+datatype_new 'a option = =: None | Some (the: 'a)
 
 datatype_new_compat option
 
@@ -52,9 +52,6 @@
 
 subsubsection {* Operations *}
 
-primrec the :: "'a option => 'a" where
-"the (Some x) = x"
-
 primrec set :: "'a option => 'a set" where
 "set None = {}" |
 "set (Some x) = {x}"