# HG changeset patch
# User blanchet
# Date 1387181878 -3600
# Node ID c3ef7b572213361defd80d2dd429a53a1e59e267
# Parent  0ef52f40d419623f355aeb0921b0eec5adc2245a
made SML/NJ happy

diff -r 0ef52f40d419 -r c3ef7b572213 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- 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