diff -r 6f43714517ee -r 08c8dad8e399 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -186,8 +186,8 @@
 
 fun is_symid str =
   (case try Symbol.explode str of
-    Some [s] => Symbol.is_symbolic s orelse is_sym_char s
-  | Some ss => forall is_sym_char ss
+    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
+  | SOME ss => forall is_sym_char ss
   | _ => false);
 
 val is_sid = is_symid orf Syntax.is_identifier;
@@ -282,7 +282,7 @@
 
 fun source do_recover get_lex pos src =
   Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
-    (if do_recover then Some recover else None) src;
+    (if do_recover then SOME recover else NONE) src;
 
 fun source_proper src = src |> Source.filter is_proper;