src/Pure/Isar/isar_output.ML

--- a/src/Pure/Isar/isar_output.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Pure/Isar/isar_output.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -66,7 +66,7 @@
   else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name);
   Symtab.update ((name, x), tab));
 
-fun add_items kind xs tab = foldl (add_item kind) (tab, xs);
+fun add_items kind xs tab = Library.foldl (add_item kind) (tab, xs);
 
 in
 
@@ -200,7 +200,7 @@
       T.is_kind T.Command tk andalso T.val_of tk mem !hidden_commands
   | is_hidden _ = false;
 
-fun filter_newlines toks = (case mapfilter
+fun filter_newlines toks = (case List.mapPartial
     (fn (tk, i) => if is_newline tk then SOME tk else NONE) toks of
   [] => [] | [tk] => [tk] | _ :: toks' => toks');
 
@@ -209,7 +209,7 @@
    ((if !hide_commands andalso exists (is_hidden o fst) toks then []
      else if !hide_commands andalso is_proof state then
        if is_proof state' then [] else filter_newlines toks
-     else mapfilter (fn (tk, i) =>
+     else List.mapPartial (fn (tk, i) =>
        if i > ! interest_level then NONE else SOME tk) toks)
     |> map (apsnd (eval_antiquote lex state'))
     |> Latex.output_tokens