src/HOL/Option.thy

--- a/src/HOL/Option.thy	Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Option.thy	Fri Jul 24 13:03:20 1998 +0200
@@ -6,7 +6,7 @@
 Datatype 'a option
 *)
 
-Option = Arith +
+Option = Datatype +
 
 datatype 'a option = None | Some 'a
 
@@ -22,8 +22,7 @@
 
   o2s	   :: "'a option => 'a set"
 
-primrec o2s option
-
+primrec
  "o2s  None    = {}"
  "o2s (Some x) = {x}"