| changeset 43061 | 8096eec997a9 |
| parent 43028 | 1c451bbb3ad7 |
| child 46961 | 5c6955f487e5 |
--- 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 (