--- a/src/HOL/Option.thy Thu Jan 23 19:02:22 2014 +0100 +++ b/src/HOL/Option.thy Fri Jan 24 11:51:45 2014 +0100 @@ -233,4 +233,3 @@ Option None Some end -