--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Mon Dec 16 08:35:03 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Mon Dec 16 09:17:58 2013 +0100
@@ -69,8 +69,8 @@
val atom_eq = is_equal o Atom.ord
val clause_ord = dict_ord Atom.ord
val clause_eq = is_equal o clause_ord
-val direct_sequent_ord = prod_ord clause_ord clause_ord o pairself snd
-val direct_sequent_eq = is_equal o direct_sequent_ord
+fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (pairself snd seqp)
+fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp)
fun make_refute_graph bot infers =
let