--- 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
--- 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
--- a/src/Provers/order.ML Mon Jan 08 16:06:16 2018 +0100
+++ b/src/Provers/order.ML Mon Jan 08 16:45:30 2018 +0100
@@ -687,7 +687,7 @@
(* DFS on the graph; apply dfs_visit to each vertex in
the graph, checking first to make sure the vertex is
as yet unvisited. *)
- app (fn u => if been_visited u then ()
+ List.app (fn u => if been_visited u then ()
else (dfs_visit G u; ())) (members G);
visited := [];
@@ -765,7 +765,7 @@
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
in if been_visited v then ()
- else (app (fn (v',l) => if been_visited v' then () else (
+ else (List.app (fn (v',l) => if been_visited v' then () else (
update (v',l);
dfs_visit v'; ()) )) (adjacent eq_comp g u')
end
--- a/src/Provers/quasi.ML Mon Jan 08 16:06:16 2018 +0100
+++ b/src/Provers/quasi.ML Mon Jan 08 16:45:30 2018 +0100
@@ -361,7 +361,7 @@
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
in if been_visited v then ()
- else (app (fn (v',l) => if been_visited v' then () else (
+ else (List.app (fn (v',l) => if been_visited v' then () else (
update (v',l);
dfs_visit v'; ()) )) (adjacent eq_comp g u')
end
--- a/src/Provers/trancl.ML Mon Jan 08 16:06:16 2018 +0100
+++ b/src/Provers/trancl.ML Mon Jan 08 16:45:30 2018 +0100
@@ -287,7 +287,7 @@
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
in if been_visited v then ()
- else (app (fn (v',l) => if been_visited v' then () else (
+ else (List.app (fn (v',l) => if been_visited v' then () else (
update (v',l);
dfs_visit v'; ()) )) (adjacent eq_comp g u')
end