--- 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