--- a/src/HOL/Option.thy Wed Sep 09 17:21:33 1998 +0200 +++ b/src/HOL/Option.thy Wed Sep 09 17:23:42 1998 +0200 @@ -23,6 +23,7 @@ o2s :: "'a option => 'a set" primrec + "o2s None = {}" "o2s (Some x) = {x}"