# HG changeset patch
# User smolkas
# Date 1373451911 -7200
# Node ID 92ed2926596d91e689f397db94ad86186e290bc8
# Parent  c8357085217c1735473271524a21b9bd8727b818
made SML/NJ happy

diff -r c8357085217c -r 92ed2926596d src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Tue Jul 09 18:45:06 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed Jul 10 12:25:11 2013 +0200
@@ -114,7 +114,7 @@
 
 (** canonical proof labels: 1, 2, 3, ... in post traversal order **)
 
-val canonical_label_ord = pairself snd #> int_ord
+fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
 
 structure Canonical_Lbl_Tab = Table(
   type key = label