src/Pure/Thy/thy_scan.ML

 
 (** scanners **)
 
 (* diagnostics *)
 
-fun lex_err None msg = "Outer lexical error: " ^ msg
-  | lex_err (Some n) msg = "Outer lexical error on line " ^ string_of_int n ^ ": " ^ msg;
+fun lex_err NONE msg = "Outer lexical error: " ^ msg
+  | lex_err (SOME n) msg = "Outer lexical error on line " ^ string_of_int n ^ ": " ^ msg;
 
 
 (* line numbering *)
 
 val incr = apsome (fn n:int => n + 1);

     (Scan.pass 0 (Scan.repeat scan_cmt) |-- keep_line ($$ "*" -- $$ ")") >> K "");
 
 
 (* scan token *)
 
-fun token k None x = (k, x, 0)
-  | token k (Some n) x = (k, x, n);
+fun token k NONE x = (k, x, 0)
+  | token k (SOME n) x = (k, x, n);
 
 fun scan_tok lex (n, cs) =
  (scan_string >> token String n ||
   scan_verbatim >> token Verbatim n ||
   Scan.repeat1 scan_blank >> (token Ignore n o implode) ||

 
 val scan_rest = Scan.any Symbol.not_eof >> implode;
 
 fun scan_token lex x =
   (case scan_tok lex x of
-    ((Keyword, "ML", n), x') => (keep_line scan_rest >> token Verbatim (Some n)) x'
+    ((Keyword, "ML", n), x') => (keep_line scan_rest >> token Verbatim (SOME n)) x'
   | tok_x' => tok_x');
 
 
 (* tokenize *)
 
 fun tokenize lex chs =
   let
     val scan_toks = Scan.repeat (scan_token lex);
     val ignore = fn (Ignore, _, _) => true | _ => false;
   in
-    (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
+    (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (SOME 1, chs) of
       (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
     | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (Symbol.beginning 10 cs))))
   end;