# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID 8096eec997a90a92c795288884bac66fafcbbb8f
# Parent  e998e85e41ff3f858521cdc188c70a7d1815184a
make SML/NJ happy

diff -r e998e85e41ff -r 8096eec997a9 src/Tools/try.ML
--- a/src/Tools/try.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/Tools/try.ML	Mon May 30 17:00:38 2011 +0200
@@ -54,7 +54,8 @@
 
 (* configuration *)
 
-val tool_ord = prod_ord int_ord string_ord o pairself (swap o apsnd #1)
+fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
+  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
 
 structure Data = Theory_Data
 (