# HG changeset patch
# User blanchet
# Date 1384440006 -3600
# Node ID e98996c2a32c61f5b264d0e773ce5c7c3270d38d
# Parent  e9ff6a25aaa6d2a666b248076d34df3305229722
made SML/NJ happy

diff -r e9ff6a25aaa6 -r e98996c2a32c src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Nov 14 15:40:06 2013 +0100
+++ b/src/HOL/Tools/try0.ML	Thu Nov 14 15:40:06 2013 +0100
@@ -110,8 +110,9 @@
   let
     val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
       Config.put Lin_Arith.verbose false)
+    fun trd (_, _, t) = t
     fun par_map f =
-      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself #3)
+      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself trd)
       else Par_List.get_some f #> the_list
   in
     if mode = Normal then