# HG changeset patch
# User blanchet
# Date 1327655995 -3600
# Node ID c59b8560eb48b33e0fbf598536004d327cc9a348
# Parent  ab9d96cc7a991493a4a7cd27606362c5542f3156
made SML/NJ happy

diff -r ab9d96cc7a99 -r c59b8560eb48 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Jan 27 10:19:55 2012 +0100
@@ -248,9 +248,9 @@
     | command =>
       "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
 
-val split_used_facts =
-  List.partition (fn (_, (sc, _)) => sc = Chained)
-  #> pairself (sort_distinct (string_ord o pairself fst))
+fun split_used_facts facts =
+  facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
+        |> pairself (sort_distinct (string_ord o pairself fst))
 
 fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
                          subgoal, subgoal_count) =