# HG changeset patch
# User blanchet
# Date 1361445746 -3600
# Node ID 7d08487aa603e725ac861525f624aef23596ce60
# Parent  2bbcc9cc12b46f2e0a65170e65ba2076959e545b
tuning

diff -r 2bbcc9cc12b4 -r 7d08487aa603 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 17:42:20 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Thu Feb 21 12:22:26 2013 +0100
@@ -67,10 +67,11 @@
 
 type direct_proof = direct_inference list
 
-fun atom_eq p = (Atom.ord p = EQUAL)
-fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d))
-fun direct_sequent_eq ((gamma, c), (delta, d)) =
-  clause_eq (gamma, delta) andalso clause_eq (c, d)
+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
+val direct_sequent_eq = is_equal o direct_sequent_ord
 
 fun make_refute_graph bot infers =
   let