src/Pure/Isar/outer_syntax.ML

 (*Note: the syntax for files is statically determined at the very
   beginning; for interactive processing it may change dynamically.*)
 
 fun get_lexicons () = ! global_lexicons;
 fun get_parsers () = ! global_parsers;
-fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
+fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (! global_parsers);
 
 fun is_markup kind name =
   (case assoc (! global_markups, name) of SOME k => k = kind | NONE => false);
 fun markup kind = Scan.one (T.is_kind T.Command andf is_markup kind o T.val_of);
 

  (if is_none (Symtab.lookup (tab, name)) then ()
   else warning ("Redefined outer syntax command " ^ quote name);
   Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
 
 fun add_parsers parsers =
-  (change_parsers (fn tab => foldl add_parser (tab, parsers));
+  (change_parsers (fn tab => Library.foldl add_parser (tab, parsers));
     change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex
       (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))));
 
 end;
 

 
 fun print_outer_syntax () =
   let
     fun pretty_cmd (name, comment, _, _) =
       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
-    val (int_cmds, cmds) = partition #4 (dest_parsers ());
+    val (int_cmds, cmds) = List.partition #4 (dest_parsers ());
   in
     [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
       Pretty.big_list "proper commands:" (map pretty_cmd cmds),
       Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)]
     |> Pretty.chunks |> Pretty.writeln

 
 fun read toks =
   Source.of_list toks
   |> toplevel_source false true true get_parser
   |> Source.exhaust
-  |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
+  |> map (fn tr => (Toplevel.name_of tr, valOf (Toplevel.source_of tr), tr));
 
 
 (** read theory **)
 
 (* check_text *)

   let
     val src = Source.of_string (File.read path);
     val pos = Path.position path;
     val (name', parents, files) = ThyHeader.scan (src, pos);
     val ml_path = ThyLoad.ml_path name;
-    val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
+    val ml_file = if ml andalso isSome (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
   in
     if name <> name' then
       error ("Filename " ^ quote (Path.pack path) ^
         " does not agree with theory name " ^ quote name')
     else (parents, map (Path.unpack o #1) files @ ml_file)