# HG changeset patch
# User wenzelm
# Date 1515426330 -3600
# Node ID c2dfc510a38c6b0f33a6f980e132f73b986ec89f
# Parent  2ebd0ef3a6b6a1431abffea5c43e9e601a44dde0
prefer qualified names;

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
diff -r 2ebd0ef3a6b6 -r c2dfc510a38c src/HOL/Tools/Metis/metis_tactic.ML
--- 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
diff -r 2ebd0ef3a6b6 -r c2dfc510a38c src/Provers/order.ML
--- 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
diff -r 2ebd0ef3a6b6 -r c2dfc510a38c src/Provers/quasi.ML
--- 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
diff -r 2ebd0ef3a6b6 -r c2dfc510a38c src/Provers/trancl.ML
--- 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