author | blanchet |
Mon, 30 May 2011 17:00:38 +0200 | |
changeset 43061 | 8096eec997a9 |
parent 43060 | e998e85e41ff |
child 43062 | 2834548a7a48 |
src/Tools/try.ML | file | annotate | diff | comparison | revisions |
--- 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 (