src/HOL/Tools/Metis/metis_tactic.ML

              (0 upto length ths0 - 1) ths0
       val ths = maps (snd o snd) th_cls_pairs
       val dischargers = map (fst o snd) th_cls_pairs
       val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
       val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
-      val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
+      val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
       val type_enc = type_enc_of_string Strict type_enc
       val (sym_tab, axioms, ord_info, concealed) =
         generate_metis_problem ctxt type_enc lam_trans cls ths
       fun get_isa_thm mth Isa_Reflexive_or_Trivial =

         | get_isa_thm mth Isa_Lambda_Lifted =
           lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
         | get_isa_thm _ (Isa_Raw ith) = ith
       val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
       val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
-      val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
+      val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
       val _ = trace_msg ctxt (K "METIS CLAUSES")
-      val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
+      val _ = List.app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
       val _ = trace_msg ctxt (K "START METIS PROVE PROCESS")
       val ordering =
         if Config.get ctxt advisory_simp then
           kbo_advisory_simp_ordering (ord_info ())
         else

                       (*add constraints arising from converting goal to clause form*)
          val proof = Metis_Proof.proof mth
          val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms
          val used = map_filter (used_axioms axioms) proof
          val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
-         val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
+         val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
          val (used_th_cls_pairs, unused_th_cls_pairs) =
            List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
          val unused_ths = maps (snd o snd) unused_th_cls_pairs
          val unused_names = map fst unused_th_cls_pairs
        in