--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Jan 08 16:06:16 2018 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Jan 08 16:45:30 2018 +0100
@@ -162,7 +162,7 @@
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) =
@@ -174,9 +174,9 @@
| 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
@@ -202,7 +202,7 @@
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