1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -132,18 +132,18 @@
     1.4  
     1.5  fun body cmd trc (name, _) =
     1.6    (case cmd name of
     1.7 -    Some (int_only, parse) =>
     1.8 +    SOME (int_only, parse) =>
     1.9        P.!!! (Scan.prompt (name ^ "# ") (trace trc parse >> pair int_only))
    1.10 -  | None => sys_error ("no parser for outer syntax command " ^ quote name));
    1.11 +  | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
    1.12  
    1.13  in
    1.14  
    1.15  fun command do_terminate do_trace cmd =
    1.16 -  P.semicolon >> K None ||
    1.17 -  P.sync >> K None ||
    1.18 +  P.semicolon >> K NONE ||
    1.19 +  P.sync >> K NONE ||
    1.20    (P.position P.command :-- body cmd do_trace) --| terminate do_terminate
    1.21      >> (fn ((name, pos), (int_only, f)) =>
    1.22 -      Some (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    1.23 +      SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    1.24          Toplevel.interactive int_only |> f));
    1.25  
    1.26  end;
    1.27 @@ -167,7 +167,7 @@
    1.28      | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
    1.29    end;
    1.30  
    1.31 -fun get_markup (ms, (name, (_, Some m))) = (name, m) :: ms
    1.32 +fun get_markup (ms, (name, (_, SOME m))) = (name, m) :: ms
    1.33    | get_markup (ms, _) = ms;
    1.34  
    1.35  fun make_markups () = global_markups := Symtab.foldl get_markup ([], ! global_parsers);
    1.36 @@ -186,7 +186,7 @@
    1.37  fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
    1.38  
    1.39  fun is_markup kind name =
    1.40 -  (case assoc (! global_markups, name) of Some k => k = kind | None => false);
    1.41 +  (case assoc (! global_markups, name) of SOME k => k = kind | NONE => false);
    1.42  fun markup kind = Scan.one (T.is_kind T.Command andf is_markup kind o T.val_of);
    1.43  
    1.44  
    1.45 @@ -241,16 +241,16 @@
    1.46    let
    1.47      val no_terminator =
    1.48        Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
    1.49 -    fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None]) x;
    1.50 +    fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]) x;
    1.51    in
    1.52      src
    1.53      |> T.source_proper
    1.54      |> Source.source T.stopper
    1.55 -      (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K None || P.not_eof >> Some))
    1.56 -      (if do_recover then Some recover else None)
    1.57 +      (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
    1.58 +      (if do_recover then SOME recover else NONE)
    1.59      |> Source.mapfilter I
    1.60      |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term trc (cmd ())) xs))
    1.61 -      (if do_recover then Some recover else None)
    1.62 +      (if do_recover then SOME recover else NONE)
    1.63      |> Source.mapfilter I
    1.64    end;
    1.65  
    1.66 @@ -296,7 +296,7 @@
    1.67      val pos = Path.position path;
    1.68      val (name', parents, files) = ThyHeader.scan (src, pos);
    1.69      val ml_path = ThyLoad.ml_path name;
    1.70 -    val ml_file = if ml andalso is_some (ThyLoad.check_file None ml_path) then [ml_path] else [];
    1.71 +    val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    1.72    in
    1.73      if name <> name' then
    1.74        error ("Filename " ^ quote (Path.pack path) ^
    1.75 @@ -315,7 +315,7 @@
    1.76      val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
    1.77      val tr_name = if time then "time_use" else "use";
    1.78    in
    1.79 -    if is_none (ThyLoad.check_file None path) then ()
    1.80 +    if is_none (ThyLoad.check_file NONE path) then ()
    1.81      else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
    1.82    end;
    1.83  
    1.84 @@ -383,9 +383,9 @@
    1.85  
    1.86  
    1.87  (*final declarations of this structure!*)
    1.88 -val command = parser false None;
    1.89 -val markup_command = parser false o Some;
    1.90 -val improper_command = parser true None;
    1.91 +val command = parser false NONE;
    1.92 +val markup_command = parser false o SOME;
    1.93 +val improper_command = parser true NONE;
    1.94  
    1.95  
    1.96  end;