diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Dec 18 16:50:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Dec 18 16:50:14 2013 +0100
@@ -68,7 +68,6 @@
 
 val atom_eq = is_equal o Atom.ord
 val clause_ord = dict_ord Atom.ord
-val clause_eq = is_equal o clause_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)