# HG changeset patch
# User wenzelm
# Date 1633166412 -7200
# Node ID baa7a208d9d55db29f6d30c89c2ca8d59220ca38
# Parent  c8c63f921741021699fb1327b7b75aeb7a0ce7d9
tuned;

diff -r c8c63f921741 -r baa7a208d9d5 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Fri Oct 01 22:48:20 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Sat Oct 02 11:20:12 2021 +0200
@@ -80,10 +80,8 @@
     \<^Const>\<open>HOL.conj for _ _\<close> => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
   | _ => [ct]);
 
-fun fold1 f = foldr1 (uncurry f);  (* FIXME !? *)
-
 val list_conj =
-  fold1 (fn c => fn c' => Thm.apply (Thm.apply \<^cterm>\<open>HOL.conj\<close> c) c');
+  foldr1 (fn (c, c') => Thm.apply (Thm.apply \<^cterm>\<open>HOL.conj\<close> c) c');
 
 fun mk_conj_tab th =
   let