src/HOL/Tools/res_reconstruct.ML

       then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines
       else let val lname = Int.toString (length deps_map)
                fun fix lno = if lno <= Vector.length thm_names
                              then SOME(Vector.sub(thm_names,lno-1))
                              else AList.lookup op= deps_map lno;
-           in  (lname, t, List.mapPartial fix (distinct (op=) deps)) ::
+           in  (lname, t, map_filter fix (distinct (op=) deps)) ::
                stringify_deps thm_names ((lno,lname)::deps_map) lines
            end;
 
 val proofstart = "proof (neg_clausify)\n";
 

         if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
         else ()
       val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
       val _ = trace "\ndecode_tstp_file: finishing\n"
   in
-    isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
+    isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
   end;
 
 
   (*=== EXTRACTING PROOF-TEXT === *)
 

     let val toks = String.tokens (not o Char.isAlphaNum)
     fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
       | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
       | inputno _ = NONE
     val lines = split_lines proofextract
-    in  List.mapPartial (inputno o toks) lines  end
+    in  map_filter (inputno o toks) lines  end
   (*String contains multiple lines. We want those of the form
     "253[0:Inp] et cetera..."
     A list consisting of the first number in each line is returned. *)
   |  get_step_nums true proofextract =
     let val toks = String.tokens (not o Char.isAlphaNum)
     fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
       | inputno _ = NONE
     val lines = split_lines proofextract
-    in  List.mapPartial (inputno o toks) lines  end
+    in  map_filter (inputno o toks) lines  end
     
   (*extracting lemmas from tstp-output between the lines from above*)
   fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
     let
     (* get the names of axioms from their numbers*)