--- a/src/HOL/Option.thy Thu Sep 11 19:26:59 2014 +0200 +++ b/src/HOL/Option.thy Thu Sep 11 19:32:36 2014 +0200 @@ -8,7 +8,7 @@ imports BNF_Least_Fixpoint Finite_Set begin -datatype_new 'a option = +datatype 'a option = None | Some (the: 'a)