src/Pure/General/basics.ML

--- a/src/Pure/General/basics.ML	Sat May 11 16:13:08 2013 +0200
+++ b/src/Pure/General/basics.ML	Sat May 11 16:57:18 2013 +0200
@@ -78,7 +78,7 @@
   | is_none NONE = true;
 
 fun the (SOME x) = x
-  | the NONE = raise Option;
+  | the NONE = raise Option.Option;
 
 fun these (SOME x) = x
   | these NONE = [];