diff -r 2ebd0ef3a6b6 -r c2dfc510a38c src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jan 08 16:06:16 2018 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jan 08 16:45:30 2018 +0100
@@ -73,9 +73,9 @@
   let
     val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
     val _ = trace_msg ctxt (fn () => "  calling type inference:")
-    val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts
+    val _ = List.app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts
     val ts' = ts |> polish_hol_terms ctxt concealed
-    val _ = app (fn t => trace_msg ctxt
+    val _ = List.app (fn t => trace_msg ctxt
                   (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
                             " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts'
   in ts' end