src/Pure/General/source.ML

--- a/src/Pure/General/source.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Pure/General/source.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -72,8 +72,8 @@
 
 fun get_single src =
   (case get src of
-    ([], _) => None
-  | (x :: xs, src') => Some (x, unget (xs, src')));
+    ([], _) => NONE
+  | (x :: xs, src') => SOME (x, unget (xs, src')));
 
 fun exhaust src =
   (case get src of
@@ -93,7 +93,7 @@
   end;
 
 fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f);
-fun filter pred = mapfilter (fn x => if pred x then Some x else None);
+fun filter pred = mapfilter (fn x => if pred x then SOME x else NONE);