1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -183,7 +183,7 @@
     1.4  
     1.5  fun get_lexicons () = ! global_lexicons;
     1.6  fun get_parsers () = ! global_parsers;
     1.7 -fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
     1.8 +fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (! global_parsers);
     1.9  
    1.10  fun is_markup kind name =
    1.11    (case assoc (! global_markups, name) of SOME k => k = kind | NONE => false);
    1.12 @@ -201,7 +201,7 @@
    1.13    Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
    1.14  
    1.15  fun add_parsers parsers =
    1.16 -  (change_parsers (fn tab => foldl add_parser (tab, parsers));
    1.17 +  (change_parsers (fn tab => Library.foldl add_parser (tab, parsers));
    1.18      change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex
    1.19        (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))));
    1.20  
    1.21 @@ -221,7 +221,7 @@
    1.22    let
    1.23      fun pretty_cmd (name, comment, _, _) =
    1.24        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    1.25 -    val (int_cmds, cmds) = partition #4 (dest_parsers ());
    1.26 +    val (int_cmds, cmds) = List.partition #4 (dest_parsers ());
    1.27    in
    1.28      [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
    1.29        Pretty.big_list "proper commands:" (map pretty_cmd cmds),
    1.30 @@ -277,7 +277,7 @@
    1.31    Source.of_list toks
    1.32    |> toplevel_source false true true get_parser
    1.33    |> Source.exhaust
    1.34 -  |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
    1.35 +  |> map (fn tr => (Toplevel.name_of tr, valOf (Toplevel.source_of tr), tr));
    1.36  
    1.37  
    1.38  (** read theory **)
    1.39 @@ -296,7 +296,7 @@
    1.40      val pos = Path.position path;
    1.41      val (name', parents, files) = ThyHeader.scan (src, pos);
    1.42      val ml_path = ThyLoad.ml_path name;
    1.43 -    val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    1.44 +    val ml_file = if ml andalso isSome (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    1.45    in
    1.46      if name <> name' then
    1.47        error ("Filename " ^ quote (Path.pack path) ^