# HG changeset patch
# User blanchet
# Date 1337079975 -7200
# Node ID fb2bc5a1eb32ba6b41c0a74a3fce0dc2db87dda6
# Parent  c35238d19bb967a9db11a3b57d23dbd7c0e412d0
made SML/NJ happy

diff -r c35238d19bb9 -r fb2bc5a1eb32 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Tue May 15 13:06:15 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Tue May 15 13:06:15 2012 +0200
@@ -96,8 +96,8 @@
 fun string_of_sequent (gamma, c) =
   string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c
 
-val string_of_ref_graph =
-  sequents_of_ref_graph #> map string_of_sequent #> cat_lines
+fun string_of_ref_graph ref_graph =
+  ref_graph |> sequents_of_ref_graph |> map string_of_sequent |> cat_lines
 
 fun redirect_sequent tainted bot (gamma, c) =
   if member atom_eq tainted c then