# HG changeset patch
# User blanchet
# Date 1323941930 -3600
# Node ID bfb5234a70bac352c5bd84530bda5ffd3f7727f6
# Parent  728cc85534713f4a1d4dace8eda73e810e014ebe
made SML/NJ happier

diff -r 728cc8553471 -r bfb5234a70ba src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Dec 15 09:13:32 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Dec 15 10:38:50 2011 +0100
@@ -75,10 +75,11 @@
 open ATP_Proof
 open ATP_Translate
 
-structure String_Redirect =
-  ATP_Redirect(type key = step_name
-               val ord = fast_string_ord o pairself fst
-               val string_of = fst)
+structure String_Redirect = ATP_Redirect(
+    type key = step_name
+    val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
+    val string_of = fst)
+
 open String_Redirect
 
 datatype reconstructor =